10 files changed, 215 insertions, 0 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 32e245e362..33b4023272 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -519,6 +519,7 @@ $(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG)
 	@echo "TEST      $<"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
+	  export BIN="$(BIN)"; \
 	  export coqc="$(coqc)"; \
 	  export coqtop="$(coqtop)"; \
 	  export coqdep="$(coqdep)"; \
diff --git a/test-suite/bugs/closed/5012.v b/test-suite/bugs/closed/5012.v
new file mode 100644
index 0000000000..5326c0fbb1
--- /dev/null
+++ b/test-suite/bugs/closed/5012.v
@@ -0,0 +1,17 @@
+Class Foo := { foo : Set }.
+
+Axiom admit : forall {T}, T.
+
+Global Instance Foo0 : Foo
+  := {| foo := admit |}.
+
+Global Instance Foo1 : Foo
+  := { foo := admit }.
+
+Existing Class Foo.
+
+Global Instance Foo2 : Foo
+  := { foo := admit }. (* Error: Unbound method name foo of class Foo. *)
+
+Set Warnings "+already-existing-class".
+Fail Existing Class Foo.
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/7695.v b/test-suite/bugs/closed/7695.v
new file mode 100644
index 0000000000..42bdb076b6
--- /dev/null
+++ b/test-suite/bugs/closed/7695.v
@@ -0,0 +1,20 @@
+Require Import Hurkens.
+
+Universes i j k.
+Module Type T.
+  Parameter T1 : Type@{i+1}.
+  Parameter e : Type@{j} = T1 : Type@{k}.
+End T.
+
+Module M.
+  Definition T1 := Type@{j}.
+  Definition e : Type@{j} = T1 : Type@{k} := eq_refl.
+End M.
+
+Module F (A:T).
+  Definition bad := TypeNeqSmallType.paradox _ A.e.
+End F.
+
+Set Printing Universes.
+Fail Module X := F M.
+(* Universe inconsistency. Cannot enforce j <= i because i < Coq.Logic.Hurkens.105 = j. *)
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/misc/7704.sh b/test-suite/misc/7704.sh
new file mode 100755
index 0000000000..0ca2c97d24
--- /dev/null
+++ b/test-suite/misc/7704.sh
@@ -0,0 +1,7 @@
+#!/usr/bin/env bash
+
+set -e
+
+export PATH=$BIN:$PATH
+
+${coqtop#"$BIN"} -compile misc/aux7704.v
diff --git a/test-suite/misc/aux7704.v b/test-suite/misc/aux7704.v
new file mode 100644
index 0000000000..6fdcf67684
--- /dev/null
+++ b/test-suite/misc/aux7704.v
@@ -0,0 +1,6 @@
+
+Goal True /\ True.
+Proof.
+  split.
+  par:exact I.
+Qed.
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.