7 files changed, 76 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4708.v b/test-suite/bugs/closed/4708.v
new file mode 100644
index 000000000..ad2e58100
--- /dev/null
+++ b/test-suite/bugs/closed/4708.v
@@ -0,0 +1,8 @@
+(*Doc, it hurts when I poke myself.*)
+
+Notation "'" := 1. (* was:
+Setting notation at level 0.
+Toplevel input, characters 0-18:
+> Notation "'" := 1.
+> ^^^^^^^^^^^^^^^^^^
+Anomaly: Uncaught exception Invalid_argument("index out of bounds"). Please report. *)
diff --git a/test-suite/bugs/closed/4718.v b/test-suite/bugs/closed/4718.v
new file mode 100644
index 000000000..12a4e8fc1
--- /dev/null
+++ b/test-suite/bugs/closed/4718.v
@@ -0,0 +1,15 @@
+(*Congruence is weaker than reflexivity when it comes to higher level than necessary equalities:*)
+
+Goal @eq Set nat nat.
+congruence.
+Qed.
+
+Goal @eq Type nat nat.
+congruence. (*bug*)
+Qed.
+
+Variable T : Type.
+
+Goal @eq Type T T.
+congruence.
+Qed.
diff --git a/test-suite/bugs/closed/4722.v b/test-suite/bugs/closed/4722.v
new file mode 100644
index 000000000..f047624c8
--- /dev/null
+++ b/test-suite/bugs/closed/4722.v
@@ -0,0 +1 @@
+(* -*- coq-prog-args: ("-emacs" "-R" "4722" "Foo") -*- *)
diff --git a/test-suite/bugs/closed/4722/tata b/test-suite/bugs/closed/4722/tata
new file mode 120000
index 000000000..b38e66e75
--- /dev/null
+++ b/test-suite/bugs/closed/4722/tata
@@ -0,0 +1 @@
+toto
+\ No newline at end of file
diff --git a/test-suite/bugs/closed/4727.v b/test-suite/bugs/closed/4727.v
new file mode 100644
index 000000000..3854bbffd
--- /dev/null
+++ b/test-suite/bugs/closed/4727.v
@@ -0,0 +1,10 @@
+(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
+Goal forall (P : Set) (l : P) (P0 : Set) (w w0 : P0) (T : Type) (a : P * T) (o : P -> option P0),
+    (forall (l1 l2 : P) (w1 : P0), o l1 = Some w1 -> o l2 = Some w1 -> l1 = l2) ->
+    o l = Some w -> o (fst a) = Some w0 -> {w = w0} + {w <> w0} -> False.
+Proof.
+  clear; intros ???????? inj H0 H1 H2.
+  destruct H2; intuition subst.
+  eapply inj in H1; [ | eauto ].
+  progress subst. (* should succeed, used to not succeed *)
+Abort.
diff --git a/test-suite/bugs/closed/4745.v b/test-suite/bugs/closed/4745.v
new file mode 100644
index 000000000..c090125e6
--- /dev/null
+++ b/test-suite/bugs/closed/4745.v
@@ -0,0 +1,35 @@
+(*I get an Anomaly in the following code.
+
+```*)
+Require Vector.
+
+Module M.
+  Lemma Vector_map_map :
+    forall A B C (f : A -> B) (g : B -> C) n (v : Vector.t A n),
+      Vector.map g (Vector.map f v) = Vector.map (fun a => g (f a)) v.
+  Proof.
+    induction v; simpl; auto using f_equal.
+  Qed.
+
+  Lemma Vector_map_map_transparent :
+    forall A B C (f : A -> B) (g : B -> C) n (v : Vector.t A n),
+      Vector.map g (Vector.map f v) = Vector.map (fun a => g (f a)) v.
+  Proof.
+    induction v; simpl; auto using f_equal.
+  Defined.
+  (* Anomaly: constant not found in kind_of_head: Coq.Vectors.Vector.t_ind. Please report. *)
+
+  (* strangely, explicitly passing the principle to induction works *)
+  Lemma Vector_map_map_transparent' :
+    forall A B C (f : A -> B) (g : B -> C) n (v : Vector.t A n),
+      Vector.map g (Vector.map f v) = Vector.map (fun a => g (f a)) v.
+  Proof.
+    induction v using Vector.t_ind; simpl; auto using f_equal.
+  Defined.
+End M.
+(*```
+
+Changing any of the following things eliminates the Anomaly
+   * moving the lemma out of the module M to the top level
+   * proving the lemma as a Fixpoint instead of using induction
+   * proving the analogous lemma on lists instead of vectors*)
diff --git a/test-suite/bugs/closed/4772.v b/test-suite/bugs/closed/4772.v
new file mode 100644
index 000000000..c3109fa31
--- /dev/null
+++ b/test-suite/bugs/closed/4772.v
@@ -0,0 +1,6 @@
+
+Record TruncType := BuildTruncType {
+  trunctype_type : Type
+}.
+
+Fail Arguments BuildTruncType _ _ {_}. (* This should fail *)