7 files changed, 72 insertions, 4 deletions
diff --git a/test-suite/bugs/closed/bug_10097.v b/test-suite/bugs/closed/bug_10097.v
new file mode 100644
index 0000000000..12f2d4cc58
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10097.v
@@ -0,0 +1,14 @@
+From Ltac2 Require Import Ltac2.
+
+(* #10097 *)
+Ltac2 Type s := [X(int)].
+Fail Ltac2 Type s.
+Fail Ltac2 Type s := [].
+
+Ltac2 Type r := [..].
+Fail Ltac2 Type r := [].
+
+Module Other.
+  Ltac2 Type s.
+  Ltac2 Type r := [].
+End Other.
diff --git a/test-suite/bugs/closed/bug_10116.v b/test-suite/bugs/closed/bug_10116.v
new file mode 100644
index 0000000000..58caa59786
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10116.v
@@ -0,0 +1,3 @@
+From Ltac2 Require Import Ltac2.
+
+Ltac2 Eval true :: [], false.
diff --git a/test-suite/bugs/closed/bug_10196.v b/test-suite/bugs/closed/bug_10196.v
index e2d6be56e9..d003ab323d 100644
--- a/test-suite/bugs/closed/bug_10196.v
+++ b/test-suite/bugs/closed/bug_10196.v
@@ -17,10 +17,10 @@ Fail Ltac2 Eval notUppercased2.
 
 (* And the same for open types*)
 Ltac2 Type open_type := [ .. ].
-Fail Ltac2 Type open_type ::= [ notUppercased ].
-Ltac2 Type open_type ::= [ Uppercased ].
+Fail Ltac2 Type open_type ::= [ notUppercased3 ].
+Ltac2 Type open_type ::= [ Uppercased3 ].
 
-Fail Ltac2 Eval notUppercased.
-Ltac2 Eval Uppercased.
+Fail Ltac2 Eval notUppercased3.
+Ltac2 Eval Uppercased3.
 
 Fail Ltac2 Type foo ::= [ | bar1 | bar2 ].
diff --git a/test-suite/bugs/closed/bug_10903.v b/test-suite/bugs/closed/bug_10903.v
new file mode 100644
index 0000000000..3da63dfbb0
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10903.v
@@ -0,0 +1,3 @@
+(* -*- coq-prog-args: ("-type-in-type"); -*- *)
+
+Inductive Ind : SProp := C : Ind -> Ind.
diff --git a/test-suite/bugs/closed/bug_11046.v b/test-suite/bugs/closed/bug_11046.v
new file mode 100644
index 0000000000..528cc4c8ff
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11046.v
@@ -0,0 +1,19 @@
+From Ltac2 Require Import Ltac2.
+
+Ltac2 Type t := [..].
+Ltac2 Type t ::= [A(int)].
+
+(* t cannot be extended with two constructors with the same name *)
+Fail Ltac2 Type t ::= [A(bool)].
+Fail Ltac2 Type t ::= [B | B(bool)].
+
+(* constructors cannot be shadowed in the same module *)
+Fail Ltac2 Type s := [A].
+
+(* constructors with the same name can be defined in distinct modules *)
+Module Other.
+  Ltac2 Type t ::= [A(bool)].
+End Other.
+Module YetAnother.
+  Ltac2 Type t := [A].
+End YetAnother.
diff --git a/test-suite/bugs/closed/bug_11048.v b/test-suite/bugs/closed/bug_11048.v
new file mode 100644
index 0000000000..d1211587f1
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11048.v
@@ -0,0 +1,5 @@
+
+Inductive foo (HUGE := _) (b : HUGE) A :=
+  bar (X:match _ : HUGE as T return HUGE with T => match (A : T) -> True with _ => T end end)
+  : foo b A.
+(* uncaught destKO *)
diff --git a/test-suite/bugs/closed/bug_8459.v b/test-suite/bugs/closed/bug_8459.v
new file mode 100644
index 0000000000..62c49e9ea7
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8459.v
@@ -0,0 +1,24 @@
+Require Import Coq.Vectors.Vector.
+
+Axiom exfalso : False.
+
+Fixpoint all_then_someV (n:nat) (l:Vector.t bool n) {struct l}:
+(Vector.fold_left orb false l) = false ->
+(forall p, (Vector.nth l p  ) = false).
+Proof.
+intros.
+destruct l.
+inversion p.
+revert h l H.
+set (P := fun n p => forall (h : bool) (l : t bool n),
+fold_left orb false (cons bool h n l) = false -> @eq bool (@nth bool (S n) (cons bool h n l) p) false).
+revert n p.
+fix loop 1.
+unshelve eapply (@Fin.rectS P).
++ elim exfalso.
++ unfold P.
+  intros.
+  eapply all_then_someV.
+  exact H0.
+Fail Defined.
+Abort.