6 files changed, 33 insertions, 54 deletions
diff --git a/test-suite/bugs/closed/bug_10189.v b/test-suite/bugs/closed/bug_10189.v
new file mode 100644
index 0000000000..d603bff386
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10189.v
@@ -0,0 +1,9 @@
+Definition foo : forall (x := unit) {y : nat}, nat := fun y => y.
+Check foo (y := 3). (*We fail to get implicits in the type past a let-in*)
+Definition foo' : forall (x : Set) {y : nat}, nat := fun _ y => y.
+Check foo' unit (y := 3). (* It works with a function binder *)
+
+Definition bar := let f {x} : nat -> nat := fun y => x in f (x := 3).
+(* Adding bar : nat -> nat gives implicits-in-term warning *)
+Fail Check bar (x := 3).
+(* The implicits from the type of the local definition leak to the outer term *)
diff --git a/test-suite/bugs/closed/bug_3890.v b/test-suite/bugs/closed/bug_3890.v
new file mode 100644
index 0000000000..e1823ac54c
--- /dev/null
+++ b/test-suite/bugs/closed/bug_3890.v
@@ -0,0 +1,12 @@
+Set Nested Proofs Allowed.
+
+Class Foo.
+Class Bar := b : Type.
+
+Instance foo : Foo.
+
+Instance bar : Bar.
+exact Type.
+Defined.
+
+Defined.
diff --git a/test-suite/bugs/closed/bug_4429.v b/test-suite/bugs/closed/bug_4429.v
deleted file mode 100644
index bf0e570ab8..0000000000
--- a/test-suite/bugs/closed/bug_4429.v
+++ /dev/null
@@ -1,31 +0,0 @@
-Require Import Arith.Compare_dec.
-Require Import Unicode.Utf8.
-
-Fixpoint my_nat_iter (n : nat) {A} (f : A → A) (x : A) : A :=
-  match n with
-    | O    => x
-    | S n' => f (my_nat_iter n' f x)
-  end.
-
-Definition gcd_IT_F (f : nat * nat → nat) (mn : nat * nat) : nat :=
-  match mn with
-    | (0, 0)       => 0
-    | (0, S n')    => S n'
-    | (S m', 0)    => S m'
-    | (S m', S n') =>
-      match le_gt_dec (S m') (S n') with
-        | left  _ => f (S m', S n' - S m')
-        | right _ => f (S m' - S n', S n')
-      end
-  end.
-
-Axiom max_correct_l : ∀ m n : nat, m <= max m n.
-Axiom max_correct_r : ∀ m n : nat, n <= max m n.
-
-Hint Resolve max_correct_l max_correct_r : arith.
-
-Theorem foo : ∀ p p' p'' : nat, p'' < S (max p (max p' p'')).
-Proof.
-  intros.
-  Timeout 3 eauto with arith.
-Qed.
diff --git a/test-suite/bugs/closed/bug_4580.v b/test-suite/bugs/closed/bug_4580.v
index a8a446cc9b..3f40569d61 100644
--- a/test-suite/bugs/closed/bug_4580.v
+++ b/test-suite/bugs/closed/bug_4580.v
@@ -2,6 +2,5 @@ Require Import Program.
 
 Class Foo (A : Type) := foo : A.
 
-Unset Refine Instance Mode.
 Program Instance f1 : Foo nat := S _.
 Next Obligation. exact 0. Defined.
diff --git a/test-suite/bugs/closed/bug_4638.v b/test-suite/bugs/closed/bug_4638.v
new file mode 100644
index 0000000000..951fe5302b
--- /dev/null
+++ b/test-suite/bugs/closed/bug_4638.v
@@ -0,0 +1,12 @@
+Set Nested Proofs Allowed.
+
+Class Foo.
+
+Goal True.
+
+Instance foo: Foo.
+Qed.
+
+trivial.
+
+Qed.
diff --git a/test-suite/bugs/opened/bug_3890.v b/test-suite/bugs/opened/bug_3890.v
deleted file mode 100644
index 9d83743b2a..0000000000
--- a/test-suite/bugs/opened/bug_3890.v
+++ /dev/null
@@ -1,22 +0,0 @@
-Set Nested Proofs Allowed.
-
-Class Foo.
-Class Bar := b : Type.
-
-Set Refine Instance Mode.
-Instance foo : Foo := _.
-Unset Refine Instance Mode.
-(* 1 subgoals, subgoal 1 (ID 4)
-
-  ============================
-   Foo *)
-
-Instance bar : Bar.
-exact Type.
-Defined.
-(* bar is defined *)
-
-About foo.
-(* foo not a defined object. *)
-
-Fail Defined.