Module `Implicit_quantifiers`

val declare_generalizable : local:bool -> Names.lident list option -> unit
val ids_of_list : Names.Id.t list -> Names.Id.Set.t
val destClassApp : Constrexpr.constr_expr -> (Libnames.qualid * Constrexpr.constr_expr list * Constrexpr.instance_expr option) CAst.t
val destClassAppExpl : Constrexpr.constr_expr -> (Libnames.qualid * (Constrexpr.constr_expr * Constrexpr.explicitation CAst.t option) list * Constrexpr.instance_expr option) CAst.t

val free_vars_of_constr_expr : Constrexpr.constr_expr -> ?⁠bound:Names.Id.Set.t -> Names.Id.t list -> Names.Id.t list
val free_vars_of_binders : ?⁠bound:Names.Id.Set.t -> Names.Id.t list -> Constrexpr.local_binder_expr list -> Names.Id.Set.t * Names.Id.t list

val generalizable_vars_of_glob_constr : ?⁠bound:Names.Id.Set.t -> ?⁠allowed:Names.Id.Set.t -> Glob_term.glob_constr -> Names.lident list
val make_fresh : Names.Id.Set.t -> Environ.env -> Names.Id.t -> Names.Id.t
val implicits_of_glob_constr : ?⁠with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits
val combine_params_freevar : Names.Id.Set.t -> (Names.GlobRef.t option * Constr.rel_declaration) -> Constrexpr.constr_expr * Names.Id.Set.t
val implicit_application : Names.Id.Set.t -> ?⁠allow_partial:bool -> (Names.Id.Set.t -> (Names.GlobRef.t option * Constr.rel_declaration) -> Constrexpr.constr_expr * Names.Id.Set.t) -> Constrexpr.constr_expr -> Constrexpr.constr_expr * Names.Id.Set.t

exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * Constrexpr.constr_expr list * Constr.rel_context

val mismatched_ctx_inst_err : Environ.env -> Typeclasses_errors.contexts -> Constrexpr.constr_expr list -> Constr.rel_context -> 'a