Merge PR #9314: Enrich implicits for instances

Reviewed-by: SkySkimmer

7 files changed, 24 insertions, 3 deletions

diff --git a/CHANGES.md b/CHANGES.md
index 38c197d8cc..c309002beb 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -116,7 +116,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 27d8b7390d..39c086eff5 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