Module Funind_plugin.Glob_termops

val get_pattern_id : Glob_term.cases_pattern -> Names.Id.t list
val mkGHole : unit -> 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 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