Add test suite files for 4700-4785

I didn't add any test-cases for timing-based bugs (4707, 4768, 4776,
4777, 4779, 4783), nor CoqIDE bugs (4700, 4751, 4752, 4756), nor
bugs about printing (4709, 4711, 4720, 4723, 4734, 4736, 4738, 4741,
4743, 4748, 4749, 4750, 4757, 4758, 4765, 4784).  I'm not sure what to
do with 4712, 4714, 4732, 4740.

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 *)