5 files changed, 164 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5696.v b/test-suite/bugs/closed/5696.v
new file mode 100644
index 0000000000..a20ad1b4da
--- /dev/null
+++ b/test-suite/bugs/closed/5696.v
@@ -0,0 +1,5 @@
+(* Slightly improving interpretation of Ltac subterms in notations *)
+
+Notation "'var2' x .. y = z ; e" := (ltac:(exact z), (fun x => .. (fun y => e)
+..)) (at level 200, x binder, y binder, e at level 220).
+Check (var2 a = 1; a).
diff --git a/test-suite/bugs/closed/7723.v b/test-suite/bugs/closed/7723.v
new file mode 100644
index 0000000000..2162901231
--- /dev/null
+++ b/test-suite/bugs/closed/7723.v
@@ -0,0 +1,58 @@
+Set Universe Polymorphism.
+
+Module Segfault.
+
+Inductive decision_tree : Type := .
+
+Fixpoint first_satisfying_helper {A B} (f : A -> option B) (ls : list A) : option B
+  := match ls with
+     | nil => None
+     | cons x xs
+       => match f x with
+          | Some v => Some v
+          | None => first_satisfying_helper f xs
+          end
+     end.
+
+Axiom admit : forall {T}, T.
+Definition dtree4 : option decision_tree :=
+  match first_satisfying_helper (fun pat : nat => Some pat) (cons 0 nil)
+  with
+  | Some _ => admit
+  | None => admit
+  end
+.
+Definition dtree'' := Eval vm_compute in dtree4. (* segfault *)
+
+End Segfault.
+
+Module OtherExample.
+
+Definition bar@{i} := Type@{i}.
+Definition foo@{i j} (x y z : nat) :=
+  @id Type@{j} bar@{i}.
+Eval vm_compute in foo.
+
+End OtherExample.
+
+Module LocalClosure.
+
+Definition bar@{i} := Type@{i}.
+
+Definition foo@{i j} (x y z : nat) :=
+  @id (nat -> Type@{j}) (fun _ => Type@{i}).
+Eval vm_compute in foo.
+
+End LocalClosure.
+
+Require Import Hurkens.
+Polymorphic Inductive unit := tt.
+
+Polymorphic Definition foo :=
+  let x := id tt in (x, x, Type).
+
+Lemma bad : False.
+  refine (TypeNeqSmallType.paradox (snd foo) _).
+  vm_compute.
+  Fail reflexivity.
+Abort.
diff --git a/test-suite/bugs/closed/7903.v b/test-suite/bugs/closed/7903.v
new file mode 100644
index 0000000000..55c7ee99a7
--- /dev/null
+++ b/test-suite/bugs/closed/7903.v
@@ -0,0 +1,4 @@
+(* Slightly improving interpretation of Ltac subterms in notations *)
+
+Notation bar x f := (let z := ltac:(exact 1) in (fun x : nat => f)).
+Check bar x (x + x).
diff --git a/test-suite/success/mutual_record.v b/test-suite/success/mutual_record.v
new file mode 100644
index 0000000000..77529733be
--- /dev/null
+++ b/test-suite/success/mutual_record.v
@@ -0,0 +1,57 @@
+Module M0.
+
+Inductive foo (A : Type) := Foo {
+  foo0 : option (bar A);
+  foo1 : nat;
+  foo2 := foo1 = 0;
+  foo3 : foo2;
+}
+
+with bar (A : Type) := Bar {
+  bar0 : A;
+  bar1 := 0;
+  bar2 : bar1 = 0;
+  bar3 : nat -> foo A;
+}.
+
+End M0.
+
+Module M1.
+
+Set Primitive Projections.
+
+Inductive foo (A : Type) := Foo {
+  foo0 : option (bar A);
+  foo1 : nat;
+  foo2 := foo1 = 0;
+  foo3 : foo2;
+}
+
+with bar (A : Type) := Bar {
+  bar0 : A;
+  bar1 := 0;
+  bar2 : bar1 = 0;
+  bar3 : nat -> foo A;
+}.
+
+End M1.
+
+Module M2.
+
+Set Primitive Projections.
+
+CoInductive foo (A : Type) := Foo {
+  foo0 : option (bar A);
+  foo1 : nat;
+  foo2 := foo1 = 0;
+  foo3 : foo2;
+}
+
+with bar (A : Type) := Bar {
+  bar0 : A;
+  bar1 := 0;
+  bar2 : bar1 = 0;
+  bar3 : nat -> foo A;
+}.
+
+End M2.
diff --git a/test-suite/success/vm_records.v b/test-suite/success/vm_records.v
new file mode 100644
index 0000000000..8a1544c8ea
--- /dev/null
+++ b/test-suite/success/vm_records.v
@@ -0,0 +1,40 @@
+Set Primitive Projections.
+
+Module M.
+
+CoInductive foo := Foo {
+  foo0 : foo;
+  foo1 : bar;
+}
+with bar := Bar {
+  bar0 : foo;
+  bar1 : bar;
+}.
+
+CoFixpoint f : foo := Foo f g
+with g : bar := Bar f g.
+
+Check (@eq_refl _ g.(bar0) <: f.(foo0).(foo0) = g.(bar0)).
+Check (@eq_refl _ g <: g.(bar1).(bar0).(foo1) = g).
+
+End M.
+
+Module N.
+
+Inductive foo := Foo {
+  foo0 : option foo;
+  foo1 : list bar;
+}
+with bar := Bar {
+  bar0 : option bar;
+  bar1 : list foo;
+}.
+
+Definition f_0 := Foo None nil.
+Definition g_0 := Bar None nil.
+
+Definition f := Foo (Some f_0) (cons g_0 nil).
+
+Check (@eq_refl _ f.(foo1) <: f.(foo1) = cons g_0 nil).
+
+End N.