Module Pattern

Patterns
type patvar = Names.Id.t

Cases pattern variables

type case_info_pattern = {
cip_style : Constr.case_style;
cip_ind : Names.inductive option;
cip_extensible : bool;(*

does this match end with _ => _ ?

*)
}
type constr_pattern =
| PRef of Names.GlobRef.t
| PVar of Names.Id.t
| PEvar of Evar.t * constr_pattern list
| PRel of int
| PApp of constr_pattern * constr_pattern array
| PSoApp of patvar * constr_pattern list
| PProj of Names.Projection.t * constr_pattern
| PLambda of Names.Name.t * constr_pattern * constr_pattern
| PProd of Names.Name.t * constr_pattern * constr_pattern
| PLetIn of Names.Name.t * constr_pattern * constr_pattern option * constr_pattern
| PSort of Sorts.family
| PMeta of patvar option
| PIf of constr_pattern * constr_pattern * constr_pattern
| PCase of case_info_pattern * (Names.Name.t array * constr_pattern) option * constr_pattern * (int * Names.Name.t array * constr_pattern) list(*

index of constructor, nb of args

*)
| PFix of int array * int * Names.Name.t array * constr_pattern array * constr_pattern array
| PCoFix of int * Names.Name.t array * constr_pattern array * constr_pattern array
| PInt of Uint63.t
| PFloat of Float64.t
| PArray of constr_pattern array * constr_pattern * constr_pattern

Nota : in a PCase, the array of branches might be shorter than expected, denoting the use of a final "_ => _" branch