7 files changed, 101 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5286.v b/test-suite/bugs/closed/5286.v
new file mode 100644
index 000000000..98d4e5c96
--- /dev/null
+++ b/test-suite/bugs/closed/5286.v
@@ -0,0 +1,9 @@
+Set Primitive Projections.
+
+CoInductive R := mkR { p : unit }.
+
+CoFixpoint foo := mkR tt.
+
+Check (eq_refl tt : p foo = tt).
+Check (eq_refl tt <: p foo = tt).
+Check (eq_refl tt <<: p foo = tt).
diff --git a/test-suite/bugs/closed/5726.v b/test-suite/bugs/closed/5726.v
new file mode 100644
index 000000000..53ef47357
--- /dev/null
+++ b/test-suite/bugs/closed/5726.v
@@ -0,0 +1,34 @@
+Set Universe Polymorphism.
+Set Printing Universes.
+
+Module GlobalReference.
+
+  Definition type' := Type.
+  Notation type := type'.
+  Check type@{Set}.
+
+End GlobalReference.
+
+Module TypeLiteral.
+
+  Notation type := Type.
+  Check type@{Set}.
+  Check type@{Prop}.
+
+End TypeLiteral.
+
+Module ExplicitSort.
+  Monomorphic Universe u.
+  Notation foo := Type@{u}.
+  Fail Check foo@{Set}.
+  Fail Check foo@{u}.
+
+  Notation bar := Type.
+  Check bar@{u}.
+End ExplicitSort.
+
+Module PropNotationUnsupported.
+  Notation foo := Prop.
+  Fail Check foo@{Set}.
+  Fail Check foo@{Type}.
+End PropNotationUnsupported.
diff --git a/test-suite/bugs/closed/6297.v b/test-suite/bugs/closed/6297.v
new file mode 100644
index 000000000..a28607058
--- /dev/null
+++ b/test-suite/bugs/closed/6297.v
@@ -0,0 +1,8 @@
+Set Printing Universes.
+
+(* Error: Anomaly "Uncaught exception "Anomaly: Incorrect universe Set
+   declared for inductive type, inferred level is max(Prop, Set+1)."."
+   Please report at http://coq.inria.fr/bugs/. *)
+Fail Record LTS: Set :=
+  lts { St: Set;
+        init: St }.
diff --git a/test-suite/bugs/closed/6490.v b/test-suite/bugs/closed/6490.v
new file mode 100644
index 000000000..dcf9ff29e
--- /dev/null
+++ b/test-suite/bugs/closed/6490.v
@@ -0,0 +1,4 @@
+Inductive Foo (A' := I) (B : Type) := foo : Foo B.
+
+Goal Foo True. dtauto. Qed.
+Goal Foo True. firstorder. Qed.
diff --git a/test-suite/bugs/closed/6534.v b/test-suite/bugs/closed/6534.v
new file mode 100644
index 000000000..f5013994c
--- /dev/null
+++ b/test-suite/bugs/closed/6534.v
@@ -0,0 +1,7 @@
+Goal forall x : nat, x = x.
+Proof.
+intros x.
+refine ((fun x x => _ tt) tt tt).
+let t := match goal with [ |- ?P ] => P end in
+let _ := type of t in
+idtac.
diff --git a/test-suite/bugs/closed/6617.v b/test-suite/bugs/closed/6617.v
new file mode 100644
index 000000000..9cabd62d4
--- /dev/null
+++ b/test-suite/bugs/closed/6617.v
@@ -0,0 +1,34 @@
+Definition MR {T M : Type} :=
+fun (R : M -> M -> Prop) (m : T -> M) (x y : T) => R (m x) (m y).
+
+Set Primitive Projections.
+
+Record sigma {A : Type} {B : A -> Type} : Type := sigmaI
+  { pr1 : A;  pr2 : B pr1 }.
+
+Axiom F : forall {A : Type} {R : A -> A -> Prop},
+  (forall x, (forall y, R y x -> unit) -> unit) -> forall (x : A), unit.
+
+Definition foo (A : Type) (l : list A) :=
+  let y := {| pr1 := A; pr2 := l |} in
+  let bar := MR lt (fun p : sigma =>
+                 (fix Ffix (x : list (pr1 p)) : nat :=
+                    match x with
+                    | nil => 0
+                    | cons _ x1 => S (Ffix x1)
+                    end) (pr2 p)) in
+fun (_ : bar y y) =>
+F (fun (r : sigma)
+       (X : forall q : sigma, bar q r -> unit) => tt).
+
+Definition fooT (A : Type) (l : list A) : Type :=
+  ltac:(let ty := type of (foo A l) in exact ty).
+Parameter P : forall A l, fooT A l -> Prop.
+
+Goal forall A l, P A l (foo A l).
+Proof.
+  intros; unfold foo.
+  Fail match goal with
+    | [ |- context [False]] => idtac
+  end.
+Admitted.
diff --git a/test-suite/bugs/closed/6677.v b/test-suite/bugs/closed/6677.v
new file mode 100644
index 000000000..99e47bb87
--- /dev/null
+++ b/test-suite/bugs/closed/6677.v
@@ -0,0 +1,5 @@
+Set Universe Polymorphism.
+
+Definition T@{i} := Type@{i}.
+Fail Definition U@{i} := (T@{i} <: Type@{i}).
+Fail Definition eqU@{i j} : @eq T@{j} U@{i} T@{i} := eq_refl.