Patternopsval constr_pattern_eq : Environ.env -> Pattern.constr_pattern -> Pattern.constr_pattern -> boolval subst_pattern : Environ.env -> Evd.evar_map -> Mod_subst.substitution -> Pattern.constr_pattern -> Pattern.constr_patternval subst_uninstantiated_pattern : Environ.env -> Evd.evar_map -> Mod_subst.substitution -> Pattern.uninstantiated_pattern -> Pattern.uninstantiated_patternval noccurn_pattern : int -> _ Pattern.constr_pattern_r -> 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 Rocq 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.uninstantiated_patternval 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_rval lift_pattern : int -> 'i Pattern.constr_pattern_r -> 'i Pattern.constr_pattern_rInterp genargs
type 'a pat_interp_fun = Environ.env -> Evd.evar_map -> Ltac_pretype.ltac_var_map -> 'a -> Pattern.constr_patternval interp_pattern : Pattern.uninstantiated_pattern pat_interp_funval register_interp_pat : (_, 'g, _) Genarg.genarg_type -> 'g pat_interp_fun -> unit