diff options
| author | Gaëtan Gilbert | 2019-05-23 10:03:42 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-06-11 09:55:51 +0200 |
| commit | 82663b28a04d82e89bd041efd256c4838312e587 (patch) | |
| tree | 8f1c555626ebe40090143be1b663a0fe07377caf /interp/implicit_quantifiers.mli | |
| parent | 45306c6c9c433b86406d041f58aafb7cf3a3ff82 (diff) | |
Simplify implicit_quantifiers
After removing `Instance : !type` implicit_application is only used in
constrintern. We propagate constant arguments ?allow_partial and
combine_params_freevar.
Also remove unused functions.
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 *) |