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.
---
 test-suite/bugs/closed/bug_3393.v |  1 +
 test-suite/bugs/closed/bug_3422.v |  1 +
 test-suite/bugs/closed/bug_9313.v | 13 +++++++++++++
 3 files changed, 15 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_9313.v

(limited to 'test-suite')

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