3 files changed, 71 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/bug_10298.v b/test-suite/bugs/closed/bug_10298.v
new file mode 100644
index 0000000000..ad4778cc36
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10298.v
@@ -0,0 +1,35 @@
+Set Implicit Arguments.
+
+Generalizable Variables A.
+
+Parameter val : Type.
+
+Class Enc (A:Type) :=
+  make_Enc { enc : A -> val }.
+
+Global Instance Enc_dummy : Enc unit.
+Admitted.
+
+Definition FORM := forall A (EA:Enc A) (Q:A->Prop), Prop.
+
+Axiom FORM_intro : forall F : FORM, F unit Enc_dummy (fun _ : unit => True).
+
+Definition IDF (F:FORM) : FORM := F.
+
+Parameter ID : forall (G:Prop), G -> G.
+
+Parameter EID : forall A (EA:Enc A) (F:FORM) (Q:A->Prop),
+  F _ _ Q ->
+  F _ _ Q.
+
+Lemma bla : forall F,
+  (forall A (EA:Enc A), IDF F EA (fun (X:A) => True) -> True) ->
+  True.
+Proof.
+  intros F M.
+  notypeclasses refine (M _ _ _).
+  notypeclasses refine (EID _ _ _ _).
+  eapply (ID _).
+  Unshelve.
+  + apply FORM_intro.
+Qed.
diff --git a/test-suite/bugs/closed/bug_10762.v b/test-suite/bugs/closed/bug_10762.v
new file mode 100644
index 0000000000..d3991d4d38
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10762.v
@@ -0,0 +1,30 @@
+
+Set Implicit Arguments.
+
+Generalizable Variables A B.
+Parameter val: Type.
+
+Class Enc (A:Type) : Type :=
+  make_Enc { enc : A -> val }.
+
+Hint Mode Enc + : typeclass_instances.
+
+Parameter bar : forall A (EA:Enc A), EA = EA.
+
+Parameter foo : forall (P:Prop),
+   P ->
+   P = P ->
+   True.
+
+Parameter id : forall (P:Prop),
+  P -> P.
+
+  Check enc.
+
+  Lemma test : True.
+  eapply foo; [ eapply bar | apply id]. apply id.
+  (* eapply bar introduces an unresolved typeclass evar that is no longer
+     a candidate after the application (eapply should leave typeclass goals shelved).
+     We ensure that this happens also _across_ goals in `[ | ]` and not only at `.`..
+      *)
+  Abort.
diff --git a/test-suite/bugs/opened/bug_3357.v b/test-suite/bugs/opened/bug_3357.v
index c479158877..f0e5d71811 100644
--- a/test-suite/bugs/opened/bug_3357.v
+++ b/test-suite/bugs/opened/bug_3357.v
@@ -1,4 +1,9 @@
-Notation D1 := (forall {T : Type} ( x : T ) , Type).
+(* See discussion in #668 for whether manual implicit arguments should
+   be allowed in notations or not *)
+
+Set Warnings "+syntax".
+
+Fail Notation D1 := (forall {T : Type} ( x : T ) , Type).
 
 Definition DD1 ( A : forall {T : Type} (x : T), Type ) := A 1.
 Fail Definition DD1' ( A : D1 ) := A 1. (* Toplevel input, characters 32-33: