diff options
Diffstat (limited to 'interp/implicit_quantifiers.mli')
| -rw-r--r-- | interp/implicit_quantifiers.mli | 17 |
1 files changed, 1 insertions, 16 deletions
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 437fef1753..d28d35f3a1 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -11,22 +11,14 @@ open Names open Glob_term open Constrexpr -open Libnames val declare_generalizable : local:bool -> lident list option -> unit -val ids_of_list : Id.t list -> Id.Set.t -val destClassApp : constr_expr -> (qualid * constr_expr list * instance_expr option) CAst.t -val destClassAppExpl : constr_expr -> (qualid * (constr_expr * explicitation CAst.t option) list * instance_expr option) CAst.t - (** Fragile, should be used only for construction a set of identifiers to avoid *) val free_vars_of_constr_expr : constr_expr -> ?bound:Id.Set.t -> Id.t list -> Id.t list -val free_vars_of_binders : - ?bound:Id.Set.t -> Id.t list -> local_binder_expr list -> Id.Set.t * Id.t list - (** Returns the generalizable free ids in left-to-right order with the location of their first occurrence *) @@ -37,14 +29,7 @@ val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits -val combine_params_freevar : - Id.Set.t -> GlobRef.t option * Constr.rel_declaration -> - Constrexpr.constr_expr * Id.Set.t - -val implicit_application : Id.Set.t -> ?allow_partial:bool -> - (Id.Set.t -> GlobRef.t option * Constr.rel_declaration -> - Constrexpr.constr_expr * Id.Set.t) -> - constr_expr -> constr_expr * Id.Set.t +val implicit_application : Id.Set.t -> constr_expr -> constr_expr * Id.Set.t (* Should be likely located elsewhere *) exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Constr.rel_context (* found, expected *) |