3 files changed, 31 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/7068.v b/test-suite/bugs/closed/7068.v
new file mode 100644
index 0000000000..9fadb195bf
--- /dev/null
+++ b/test-suite/bugs/closed/7068.v
@@ -0,0 +1,6 @@
+(* These tests are only about a subset of #7068 *)
+(* The original issue is still open *)
+
+Inductive foo : let T := Type in T := .
+Definition bob1 := Eval vm_compute in foo_rect.
+Definition bob2 := Eval native_compute in foo_rect.
diff --git a/test-suite/bugs/closed/7076.v b/test-suite/bugs/closed/7076.v
new file mode 100644
index 0000000000..0abc88c282
--- /dev/null
+++ b/test-suite/bugs/closed/7076.v
@@ -0,0 +1,4 @@
+(* These calls were raising an anomaly at some time *)
+Inductive A : nat -> id (nat->Type) := .
+Eval vm_compute in fun x => match x in A y z return y = z with end.
+Eval native_compute in fun x => match x in A y z return y = z with end.
diff --git a/test-suite/bugs/closed/7631.v b/test-suite/bugs/closed/7631.v
new file mode 100644
index 0000000000..34eb8b8676
--- /dev/null
+++ b/test-suite/bugs/closed/7631.v
@@ -0,0 +1,21 @@
+Module NamedContext.
+
+Definition foo := true.
+
+Section Foo.
+
+Let bar := foo.
+
+Eval native_compute in bar.
+
+End Foo.
+
+End NamedContext.
+
+Module RelContext.
+
+Definition foo := true.
+
+Definition bar (x := foo) := Eval native_compute in x.
+
+End RelContext.