Patternopsval constr_pattern_eq :
Pattern.constr_pattern ->
Pattern.constr_pattern ->
boolval subst_pattern :
Environ.env ->
Evd.evar_map ->
Mod_subst.substitution ->
Pattern.constr_pattern ->
Pattern.constr_patternval noccurn_pattern : int -> Pattern.constr_pattern -> boolhead_pattern_bound t extracts the head variable/constant of the type t or raises BoundPattern (even if a sort); it raises an anomaly if t is an abstraction
val head_pattern_bound : Pattern.constr_pattern -> Names.GlobRef.thead_of_constr_reference c assumes r denotes a reference and returns its label; raises an anomaly otherwise
val head_of_constr_reference :
Evd.evar_map ->
EConstr.constr ->
Names.GlobRef.tpattern_of_constr c translates a term c with metavariables into a pattern; currently, no destructor (Cases, Fix, Cofix) and no existential variable are allowed in c
val pattern_of_constr :
Environ.env ->
Evd.evar_map ->
EConstr.constr ->
Pattern.constr_patternval legacy_bad_pattern_of_constr :
Environ.env ->
Evd.evar_map ->
EConstr.constr ->
Pattern.constr_patternDo not use, for internal Coq use only.
pattern_of_glob_constr l c translates a term c with metavariables into a pattern; variables bound in l are replaced by the pattern to which they are bound
val pattern_of_glob_constr :
Glob_term.glob_constr ->
Names.Id.Set.t * Pattern.constr_patternval map_pattern_with_binders :
( Names.Name.t -> 'a -> 'a ) ->
( 'a -> Pattern.constr_pattern -> Pattern.constr_pattern ) ->
'a ->
Pattern.constr_pattern ->
Pattern.constr_patternval lift_pattern : int -> Pattern.constr_pattern -> Pattern.constr_pattern