Module Patternops

Functions on patterns
val constr_pattern_eq : Pattern.constr_pattern -> Pattern.constr_pattern -> bool
val occur_meta_pattern : Pattern.constr_pattern -> bool
val noccurn_pattern : int -> Pattern.constr_pattern -> bool
exception BoundPattern

head_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.t

head_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.t

pattern_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 legacy_bad_pattern_of_constr : Environ.env -> Evd.evar_map -> EConstr.constr -> Pattern.constr_pattern

Do 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 -> Pattern.patvar list * Pattern.constr_pattern
val map_pattern_with_binders : (Names.Name.t -> 'a -> 'a) -> ('a -> Pattern.constr_pattern -> Pattern.constr_pattern) -> 'a -> Pattern.constr_pattern -> Pattern.constr_pattern
val lift_pattern : int -> Pattern.constr_pattern -> Pattern.constr_pattern