Implicit_quantifiersval declare_generalizable : local:bool -> Names.lident list option -> unitFragile, should be used only for construction a set of identifiers to avoid
val free_vars_of_constr_expr : Constrexpr.constr_expr -> ?bound:Names.Id.Set.t -> Names.Id.t list -> Names.Id.t listReturns the generalizable free ids in left-to-right order with the location of their first occurrence
val generalizable_vars_of_glob_constr : ?bound:Names.Id.Set.t -> ?allowed:Names.Id.Set.t -> Glob_term.glob_constr -> Names.lident listval make_fresh : Names.Id.Set.t -> Environ.env -> Names.Id.t -> Names.Id.tval implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicitsval implicit_application : Names.Id.Set.t -> Constrexpr.constr_expr -> Constrexpr.constr_expr * Names.Id.Set.t