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 eq_cases_pattern : Environ.env -> 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 : EConstr.types -> Environ.env -> Evd.evar_map -> Glob_term.glob_constr -> Glob_term.glob_constr