Funind_plugin.Glob_termopsval get_pattern_id : Glob_term.cases_pattern -> Names.Id.t listval pattern_to_term : Glob_term.cases_pattern -> Glob_term.glob_constrval mkGRef : Names.GlobRef.t -> Glob_term.glob_constrval mkGVar : Names.Id.t -> Glob_term.glob_constrval mkGApp : (Glob_term.glob_constr * Glob_term.glob_constr list) -> Glob_term.glob_constrval mkGLambda : (Names.Name.t * Glob_term.glob_constr * Glob_term.glob_constr) -> Glob_term.glob_constrval mkGProd : (Names.Name.t * Glob_term.glob_constr * Glob_term.glob_constr) -> Glob_term.glob_constrval mkGLetIn : (Names.Name.t * Glob_term.glob_constr * Glob_term.glob_constr option * Glob_term.glob_constr) -> Glob_term.glob_constrval mkGCases : (Glob_term.glob_constr option * Glob_term.tomatch_tuples * Glob_term.cases_clauses) -> Glob_term.glob_constrval mkGHole : unit -> Glob_term.glob_constrval glob_decompose_app : Glob_term.glob_constr -> Glob_term.glob_constr * Glob_term.glob_constr listval glob_make_eq : ?typ:Glob_term.glob_constr -> Glob_term.glob_constr -> Glob_term.glob_constr -> Glob_term.glob_constrval glob_make_neq : Glob_term.glob_constr -> Glob_term.glob_constr -> Glob_term.glob_constrval change_vars : Names.Id.t Names.Id.Map.t -> Glob_term.glob_constr -> Glob_term.glob_constrval 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.tval alpha_rt : Names.Id.t list -> Glob_term.glob_constr -> Glob_term.glob_constrval alpha_br : Names.Id.t list -> Glob_term.cases_clause -> Glob_term.cases_clauseval replace_var_by_term : Names.Id.t -> Glob_term.glob_constr -> Glob_term.glob_constr -> Glob_term.glob_constrval is_free_in : Names.Id.t -> Glob_term.glob_constr -> boolval are_unifiable : Environ.env -> Glob_term.cases_pattern -> Glob_term.cases_pattern -> boolval eq_cases_pattern : Environ.env -> Glob_term.cases_pattern -> Glob_term.cases_pattern -> boolval ids_of_pat : Glob_term.cases_pattern -> Names.Id.Set.tval expand_as : Glob_term.glob_constr -> Glob_term.glob_constrval resolve_and_replace_implicits : EConstr.types -> Environ.env -> Evd.evar_map -> Glob_term.glob_constr -> Glob_term.glob_constr