From 82663b28a04d82e89bd041efd256c4838312e587 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 23 May 2019 10:03:42 +0200
Subject: 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.
---
 interp/implicit_quantifiers.mli | 17 +----------------
 1 file changed, 1 insertion(+), 16 deletions(-)

(limited to 'interp/implicit_quantifiers.mli')

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 *)
-- 
cgit v1.2.3


From 1c5e2508d6a9604ffd77eff3140a86eafbc672a9 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 23 May 2019 10:54:14 +0200
Subject: Fix #10225 (Instance := {} accepts duplicate fields)

This replaces the mismatched context error, which occurred when
Instance := {} was used with strictly more fields than declared.

Since we later check that field names match those declared for the
instance, now that we reject duplicates we know that there are no
extra fields.
---
 interp/implicit_quantifiers.mli | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'interp/implicit_quantifiers.mli')

diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index d28d35f3a1..8536a2dee0 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -30,7 +30,3 @@ 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 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 *)
-val mismatched_ctx_inst_err : Environ.env -> Typeclasses_errors.contexts -> constr_expr list -> Constr.rel_context -> 'a
-- 
cgit v1.2.3