package coq

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

type constr_under_binders = Names.Id.t list * EConstr.constr

type patvar_map = EConstr.constr Names.Id.Map.t

type extended_patvar_map = constr_under_binders Names.Id.Map.t

type case_info_pattern = {

cip_style : Misctypes.case_style;
cip_ind : Names.inductive option;
cip_ind_tags : bool list option;
cip_extensible : bool;

}

type constr_pattern =

| PRef of Globnames.global_reference
| PVar of Names.Id.t
| PEvar of Misctypes.existential_key * constr_pattern array
| PRel of int
| PApp of constr_pattern * constr_pattern array
| PSoApp of Misctypes.patvar * constr_pattern list
| PProj of Names.projection * 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 Misctypes.glob_sort
| PMeta of Misctypes.patvar option
| PIf of constr_pattern * constr_pattern * constr_pattern
| PCase of case_info_pattern * constr_pattern * constr_pattern * (int * bool list * constr_pattern) list
| PFix of Term.fixpoint
| PCoFix of Term.cofixpoint