7 files changed, 52 insertions, 1 deletions
diff --git a/test-suite/bugs/bug_11140.v b/test-suite/bugs/bug_11140.v
new file mode 100644
index 0000000000..ca806ea324
--- /dev/null
+++ b/test-suite/bugs/bug_11140.v
@@ -0,0 +1,11 @@
+Axiom T : nat -> Prop.
+Axiom f : forall x, T x.
+Arguments f & x.
+
+Lemma test : (f (1 + _) : T 2) = f 2.
+match goal with
+| |- (f (1 + 1) = f 2) => idtac
+| |- (f 2 = f 2) => fail (* Issue 11140 *)
+| |- _ => fail
+end.
+Abort.
diff --git a/test-suite/bugs/closed/bug_11133.v b/test-suite/bugs/closed/bug_11133.v
new file mode 100644
index 0000000000..87f15a4a19
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11133.v
@@ -0,0 +1,18 @@
+Module Type Universe.
+Parameter U : nat.
+End Universe.
+
+Module Univ_prop (Univ : Universe).
+Include Univ.
+End Univ_prop.
+
+Module Monad (Univ : Universe).
+Module UP := (Univ_prop Univ).
+End Monad.
+
+Module Rules (Univ:Universe).
+Module MP := Monad Univ.
+Include MP.
+Import UP.
+Definition M := UP.U.    (* anomaly here *)
+End Rules.
diff --git a/test-suite/bugs/closed/bug_11168.v b/test-suite/bugs/closed/bug_11168.v
new file mode 100644
index 0000000000..6e109e33e6
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11168.v
@@ -0,0 +1,5 @@
+Axiom f : forall T, T.
+Arguments f &.
+Check f _ _.
+Check f (_ -> _) _.
+Check f (forall x, _) _.
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/closed/bug_11360.v b/test-suite/bugs/closed/bug_11360.v
new file mode 100644
index 0000000000..d8bc4a9f02
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11360.v
@@ -0,0 +1,6 @@
+Section S.
+  Variable (A:Type).
+  #[universes(template)]
+  Inductive bar (d:A) := .
+End S.
+Check bar nat 0.
diff --git a/test-suite/bugs/closed/bug_11421.v b/test-suite/bugs/closed/bug_11421.v
new file mode 100644
index 0000000000..8ddf05c888
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11421.v
@@ -0,0 +1 @@
+Fail Definition plus1_plus1 : Type@{Set+1} := Type@{Set+1}.
diff --git a/test-suite/bugs/closed/bug_2729.v b/test-suite/bugs/closed/bug_2729.v
index ff08bdc6bb..52cc34beb3 100644
--- a/test-suite/bugs/closed/bug_2729.v
+++ b/test-suite/bugs/closed/bug_2729.v
@@ -82,7 +82,7 @@ Inductive SequenceBase (pu : PatchUniverse)
                      (p : pu_type from mid)
                      (qs : SequenceBase pu mid to),
               SequenceBase pu from to.
-Arguments Nil [pu cxt].
+Arguments Nil {pu cxt}.
 Arguments Cons [pu from mid to].
 
 Program Fixpoint insertBase {pu : PatchUniverse}