Module Recdef_plugin.Glob_termops

val get_pattern_id : Glob_term.cases_pattern -> Names.Id.t list
val pattern_to_term : Glob_term.cases_pattern -> Glob_term.glob_constr
val mkGRef : Names.GlobRef.t -> Glob_term.glob_constr
val mkGVar : Names.Id.t -> Glob_term.glob_constr
val mkGApp : (Glob_term.glob_constr * Glob_term.glob_constr list) -> Glob_term.glob_constr
val mkGLambda : (Names.Name.t * Glob_term.glob_constr * Glob_term.glob_constr) -> Glob_term.glob_constr
val mkGProd : (Names.Name.t * Glob_term.glob_constr * Glob_term.glob_constr) -> Glob_term.glob_constr
val mkGLetIn : (Names.Name.t * Glob_term.glob_constr * Glob_term.glob_constr option * Glob_term.glob_constr) -> Glob_term.glob_constr
val mkGCases : (Glob_term.glob_constr option * Glob_term.tomatch_tuples * Glob_term.cases_clauses) -> Glob_term.glob_constr
val mkGHole : unit -> Glob_term.glob_constr
val glob_decompose_app : Glob_term.glob_constr -> Glob_term.glob_constr * Glob_term.glob_constr list
val glob_make_eq : ?⁠typ:Glob_term.glob_constr -> Glob_term.glob_constr -> Glob_term.glob_constr -> Glob_term.glob_constr
val glob_make_neq : Glob_term.glob_constr -> Glob_term.glob_constr -> Glob_term.glob_constr
val change_vars : Names.Id.t Names.Id.Map.t -> Glob_term.glob_constr -> Glob_term.glob_constr
val alpha_pat : Names.Id.Map.key list -> Glob_term.cases_pattern -> Glob_term.cases_pattern * Names.Id.Map.key list * Names.Id.t Names.Id.Map.t
val alpha_rt : Names.Id.t list -> Glob_term.glob_constr -> Glob_term.glob_constr
val alpha_br : Names.Id.t list -> Glob_term.cases_clause -> Glob_term.cases_clause
val replace_var_by_term : Names.Id.t -> Glob_term.glob_constr -> Glob_term.glob_constr -> Glob_term.glob_constr
val is_free_in : Names.Id.t -> Glob_term.glob_constr -> bool
val are_unifiable : Glob_term.cases_pattern -> Glob_term.cases_pattern -> bool
val eq_cases_pattern : Glob_term.cases_pattern -> Glob_term.cases_pattern -> bool
val ids_of_pat : Glob_term.cases_pattern -> Names.Id.Set.t
val expand_as : Glob_term.glob_constr -> Glob_term.glob_constr
val resolve_and_replace_implicits : ?⁠flags:Pretyping.inference_flags -> ?⁠expected_type:Pretyping.typing_constraint -> Environ.env -> Evd.evar_map -> Glob_term.glob_constr -> Glob_term.glob_constr