Case

Ltac2.Constr.Unsafe.Case

val equal : case -> case -> bool

equal case1 case2 checks equality of the inductive components of the case info. When comparing the inductives, those obtained through module aliases or Include are not considered equal by this function.

val inductive : case -> inductive

inductive case returns the inductive type being matched on in a pattern match expression.