From 735d3fd21c65688143541d77c4153f52b963f4c4 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Sun, 6 Jan 2019 20:29:19 -0800
Subject: Enrich implicits for instances

For compatibility, also
* Adjust implicits on equiv_transitivity and equiv_symmetry, and in some closed bugs
* Add overlay for HoTT setting Arguments on some instances.
---
 CHANGES.md                        |  2 +-
 test-suite/bugs/closed/bug_3393.v |  1 +
 test-suite/bugs/closed/bug_3422.v |  1 +
 test-suite/bugs/closed/bug_9313.v | 13 +++++++++++++
 theories/Classes/CEquivalence.v   |  3 +++
 theories/Classes/Equivalence.v    |  3 +++
 vernac/classes.ml                 |  4 ++--
 7 files changed, 24 insertions(+), 3 deletions(-)
 create mode 100644 test-suite/bugs/closed/bug_9313.v

diff --git a/CHANGES.md b/CHANGES.md
index 1a0b53f84a..98440a8959 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -114,7 +114,7 @@ Vernacular commands
   avoid conflicts with explicitly named binders.
 
 - Computation of implicit arguments now properly handles local definitions in the
-  binders for an `Instance`.
+  binders for an `Instance`, and can be mixed with implicit binders `{x : T}`.
 
 - `Declare Instance` now requires an instance name.
 
diff --git a/test-suite/bugs/closed/bug_3393.v b/test-suite/bugs/closed/bug_3393.v
index d2eb61e3e2..b0b573f5d5 100644
--- a/test-suite/bugs/closed/bug_3393.v
+++ b/test-suite/bugs/closed/bug_3393.v
@@ -109,6 +109,7 @@ Global Instance isisomorphism_compose' `{Funext}
        `{@IsIsomorphism (C -> D) F F' T}
 : @IsIsomorphism (C -> D) F F'' (T' o T)%natural_transformation
   := @isisomorphism_compose (C -> D) _ _ T' _ _ T _.
+Arguments isisomorphism_compose' {H C D F' F''} T' {F} T {H0 H1}.
 Section lemmas.
   Context `{Funext}.
   Variable C : PreCategory.
diff --git a/test-suite/bugs/closed/bug_3422.v b/test-suite/bugs/closed/bug_3422.v
index 460ae8f110..1305104cdb 100644
--- a/test-suite/bugs/closed/bug_3422.v
+++ b/test-suite/bugs/closed/bug_3422.v
@@ -175,6 +175,7 @@ Global Instance isisomorphism_compose'
        `{@IsIsomorphism (C -> D) F F' T}
 : @IsIsomorphism (C -> D) F F'' (T' o T)%natural_transformation
   := @isisomorphism_compose (C -> D) _ _ T' _ _ T _.
+Arguments isisomorphism_compose' {C D F' F''} T' {F} T {H H0}.
 
 Section lemmas.
   Local Open Scope natural_transformation_scope.
diff --git a/test-suite/bugs/closed/bug_9313.v b/test-suite/bugs/closed/bug_9313.v
new file mode 100644
index 0000000000..0845e7732c
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9313.v
@@ -0,0 +1,13 @@
+Set Implicit Arguments.
+Existing Class True.
+
+Instance foo1 (a : nat) {b : nat} (e : a = b) : True := I.
+Check foo1 (a := 3) (b := 4).
+
+Definition foo2 (a : nat) {b : nat} (e : a = b) : True := I.
+Check foo2 (a := 3) (b := 4).
+
+Instance foo3 (a : nat) {b : nat} (e : a = b) : True.
+exact I.
+Qed.
+Check foo3 (a := 3) (b := 4).
diff --git a/theories/Classes/CEquivalence.v b/theories/Classes/CEquivalence.v
index c376efef2e..f04ae90950 100644
--- a/theories/Classes/CEquivalence.v
+++ b/theories/Classes/CEquivalence.v
@@ -64,6 +64,9 @@ Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv.
          now transitivity y.
   Qed.
 
+Arguments equiv_symmetric {A R} sa x y.
+Arguments equiv_transitive {A R} sa x y z.
+
 (** Use the [substitute] command which substitutes an equivalence in every hypothesis. *)
 
 Ltac setoid_subst H :=
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 516ea12099..384d041461 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -64,6 +64,9 @@ Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv | 1.
          now transitivity y.
   Qed.
 
+Arguments equiv_symmetric {A R} sa x y.
+Arguments equiv_transitive {A R} sa x y z.
+
 (** Use the [substitute] command which substitutes an equivalence in every hypothesis. *)
 
 Ltac setoid_subst H :=
diff --git a/vernac/classes.ml b/vernac/classes.ml
index dd49f09d35..a69080fb39 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -106,7 +106,7 @@ let id_of_class cl =
     | _ -> assert false
 
 let instance_hook k info global imps ?hook cst =
-  Impargs.maybe_declare_manual_implicits false cst ~enriching:false imps;
+  Impargs.maybe_declare_manual_implicits false cst imps;
   let info = intern_info info in
   Typeclasses.declare_instance (Some info) (not global) cst;
   (match hook with Some h -> h cst | None -> ())
@@ -149,7 +149,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id
   if program_mode then
     let hook _ _ vis gr =
       let cst = match gr with ConstRef kn -> kn | _ -> assert false in
-      Impargs.declare_manual_implicits false gr ~enriching:false [imps];
+      Impargs.declare_manual_implicits false gr [imps];
       let pri = intern_info pri in
       Typeclasses.declare_instance (Some pri) (not global) (ConstRef cst)
     in
-- 
cgit v1.2.3