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 'i uninstantiated_pattern =
| PGenarg : Genarg.glob_generic_argument -> [ `uninstantiated ] uninstantiated_pattern
type 'i constr_pattern_r =
| PRef of Names.GlobRef.t
| PVar of Names.Id.t
| PEvar of Evar.t * 'i constr_pattern_r list
| PRel of int
| PApp of 'i constr_pattern_r * 'i constr_pattern_r array
| PSoApp of patvar * 'i constr_pattern_r list
| PProj of Names.Projection.t * 'i constr_pattern_r
| PLambda of Names.Name.t * 'i constr_pattern_r * 'i constr_pattern_r
| PProd of Names.Name.t * 'i constr_pattern_r * 'i constr_pattern_r
| PLetIn of Names.Name.t * 'i constr_pattern_r * 'i constr_pattern_r option * 'i constr_pattern_r
| PSort of Sorts.family
| PMeta of patvar option
| PIf of 'i constr_pattern_r * 'i constr_pattern_r * 'i constr_pattern_r
| PCase of case_info_pattern * (Names.Name.t array * 'i constr_pattern_r) option * 'i constr_pattern_r * (int * Names.Name.t array * 'i constr_pattern_r) list(*

index of constructor, nb of args

*)
| PFix of int array * int * Names.Name.t array * 'i constr_pattern_r array * 'i constr_pattern_r array
| PCoFix of int * Names.Name.t array * 'i constr_pattern_r array * 'i constr_pattern_r array
| PInt of Uint63.t
| PFloat of Float64.t
| PString of Pstring.t
| PArray of 'i constr_pattern_r array * 'i constr_pattern_r * 'i constr_pattern_r
| PUninstantiated of 'i uninstantiated_pattern
type constr_pattern = [ `any ] constr_pattern_r

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

type _ pattern_kind =
| Any
| Uninstantiated : [ `uninstantiated ] pattern_kind