Module Patternops

Functions on patterns
val constr_pattern_eq : Environ.env -> Pattern.constr_pattern -> Pattern.constr_pattern -> bool
val noccurn_pattern : int -> _ Pattern.constr_pattern_r -> 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 : Environ.env -> Glob_term.glob_constr -> Names.Id.Set.t * Pattern.constr_pattern
val uninstantiated_pattern_of_glob_constr : Environ.env -> Glob_term.glob_constr -> Names.Id.Set.t * [ `uninstantiated ] Pattern.constr_pattern_r
val map_pattern_with_binders : (Names.Name.t -> 'a -> 'a) -> ('a -> 'i Pattern.constr_pattern_r -> 'i Pattern.constr_pattern_r) -> 'a -> 'i Pattern.constr_pattern_r -> 'i Pattern.constr_pattern_r
val lift_pattern : int -> 'i Pattern.constr_pattern_r -> 'i Pattern.constr_pattern_r

Interp genargs

val interp_pattern : [ `uninstantiated ] Pattern.constr_pattern_r pat_interp_fun
val register_interp_pat : (_, 'g, _) Genarg.genarg_type -> 'g pat_interp_fun -> unit