6 files changed, 102 insertions, 1 deletions
diff --git a/test-suite/bugs/bug_9490.v b/test-suite/bugs/bug_9490.v
new file mode 100644
index 0000000000..a5def40c49
--- /dev/null
+++ b/test-suite/bugs/bug_9490.v
@@ -0,0 +1,9 @@
+Declare Custom Entry with_pattern.
+Declare Custom Entry M_branch.
+Notation "'with' | p1 | .. | pn 'end'" :=
+  (cons p1 (.. (cons pn nil) ..))
+  (in custom with_pattern at level 91, p1 custom M_branch at level 202, pn custom M_branch at level 202).
+Notation "'bla'" := I (in custom M_branch at level 202).
+Notation "'[use_with'  l  ]" := (l) (at level 0, l custom with_pattern at level 91).
+Check [use_with with | bla end].
+Check [use_with with | bla | bla end].
diff --git a/test-suite/bugs/bug_9532.v b/test-suite/bugs/bug_9532.v
new file mode 100644
index 0000000000..d198d45f2f
--- /dev/null
+++ b/test-suite/bugs/bug_9532.v
@@ -0,0 +1,12 @@
+Declare Custom Entry atom.
+Notation "1" := tt (in custom atom).
+Notation "atom:( s )" := s (s custom atom).
+
+Declare Custom Entry expr.
+Notation "expr:( s )" := s (s custom expr).
+Notation "( x , y , .. , z )" :=  (@cons unit x (@cons unit y .. (@cons unit z (@nil unit)) ..))
+  (in custom expr at level 0, x custom atom, y custom atom, z custom atom).
+
+Check atom:(1).
+Check expr:((1,1)).
+Check expr:((1,1,1)).
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/closed/bug_11321.v b/test-suite/bugs/closed/bug_11321.v
new file mode 100644
index 0000000000..ce95280fb1
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11321.v
@@ -0,0 +1,10 @@
+Require Import Cyclic63.
+
+Goal False.
+Proof.
+assert (4294967296 *c 2147483648 = WW 2 0)%int63 as H.
+  vm_cast_no_check (@eq_refl (zn2z int) (WW 2 0)%int63).
+generalize (f_equal (zn2z_to_Z wB to_Z) H).
+now rewrite mulc_WW_spec.
+Fail Qed.
+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: