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.

15 files changed, 388 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 *)
diff --git a/test-suite/bugs/opened/4701.v b/test-suite/bugs/opened/4701.v
new file mode 100644
index 000000000..9286f0f1f
--- /dev/null
+++ b/test-suite/bugs/opened/4701.v
@@ -0,0 +1,23 @@
+(*Suppose we have*)
+
+  Inductive my_if {A B} : bool -> Type :=
+  | then_case (_ : A) : my_if true
+  | else_case (_ : B) : my_if false.
+  Notation "'If' b 'Then' A 'Else' B" := (@my_if A B b) (at level 10).
+
+(*then here are three inductive type declarations that work:*)
+
+  Inductive I1 :=
+  | i1 (x : I1).
+  Inductive I2 :=
+  | i2 (x : nat).
+  Inductive I3 :=
+  | i3 (b : bool) (x : If b Then I3 Else nat).
+
+(*and here is one that does not, despite being equivalent to [I3]:*)
+
+  Fail Inductive I4 :=
+  | i4 (b : bool) (x : if b then I4 else nat). (* Error: Non strictly positive occurrence of "I4" in
+   "forall b : bool, (if b then I4 else nat) -> I4". *)
+
+(*I think this one should work.  I believe this is a conservative extension over CIC: Since [match] statements returning types can always be re-encoded as inductive type families, the analysis should be independent of whether the constructor uses an inductive or a [match] statement.*)
diff --git a/test-suite/bugs/opened/4717.v b/test-suite/bugs/opened/4717.v
new file mode 100644
index 000000000..9ad474672
--- /dev/null
+++ b/test-suite/bugs/opened/4717.v
@@ -0,0 +1,19 @@
+(*See below. They sometimes work, and sometimes do not. Is this a bug?*)
+
+Require Import Omega Psatz.
+
+Definition foo := nat.
+
+Goal forall (n : foo), 0 = n - n.
+Proof. intros. omega. (* works *) Qed.
+
+Goal forall (x n : foo), x = x + n - n.
+Proof.
+  intros.
+  Fail omega. (* Omega can't solve this system *)
+  Fail lia. (* Cannot find witness. *)
+  unfold foo in *.
+  omega. (* works *)
+Qed.
+
+(* Guillaume Melquiond: What matters is the equality. In the first case, it is @eq nat. In the second case, it is @eq foo. The same issue exists for ring and field. So it is not a bug, but it is worth fixing.*)
diff --git a/test-suite/bugs/opened/4721.v b/test-suite/bugs/opened/4721.v
new file mode 100644
index 000000000..1f184b393
--- /dev/null
+++ b/test-suite/bugs/opened/4721.v
@@ -0,0 +1,13 @@
+Variables S1 S2 : Set.
+
+Goal @eq Type S1 S2 -> @eq Type S1 S2.
+intro H.
+Fail tauto.
+assumption.
+Qed.
+
+(*This is in 8.5pl1, and Matthieq Sozeau says: "That's a regression in tauto indeed, which now requires exact equality of the universes, through a non linear goal pattern matching:
+match goal with ?X1 |- ?X1 forces both instances of X1 to be convertible,
+with no additional universe constraints currently, but the two types are
+initially different. This can be fixed easily to allow the same flexibility
+as in 8.4 (or assumption) to unify the universes as well."*)
diff --git a/test-suite/bugs/opened/4728.v b/test-suite/bugs/opened/4728.v
new file mode 100644
index 000000000..230b4beb6
--- /dev/null
+++ b/test-suite/bugs/opened/4728.v
@@ -0,0 +1,72 @@
+(*I'd like the final [Check] in the following to work:*)
+
+Ltac fin_eta_expand :=
+  [ > lazymatch goal with
+      | [ H : _ |- _ ] => clear H
+      end..
+  | lazymatch goal with
+    | [ H : ?T |- ?T ]
+      => exact H
+    | [ |- ?G ]
+      => fail 0 "No hypothesis matching" G
+    end ];
+  let n := numgoals in
+  tryif constr_eq numgoals 0
+  then idtac
+  else fin_eta_expand.
+
+Ltac pre_eta_expand x :=
+  let T := type of x in
+  let G := match goal with |- ?G => G end in
+  unify T G;
+  unshelve econstructor;
+  destruct x;
+  fin_eta_expand.
+
+Ltac eta_expand x :=
+  let v := constr:(ltac:(pre_eta_expand x)) in
+  idtac v;
+  let v := (eval cbv beta iota zeta in v) in
+  exact v.
+
+Notation eta_expand x := (ltac:(eta_expand x)) (only parsing).
+
+Ltac partial_unify eqn :=
+  lazymatch eqn with
+  | ?x = ?x => idtac
+  | ?f ?x = ?g ?y
+    => partial_unify (f = g);
+       (tryif unify x y then
+           idtac
+         else tryif has_evar x then
+             unify x y
+           else tryif has_evar y then
+               unify x y
+             else
+               idtac)
+  | ?x = ?y
+    => idtac;
+       (tryif unify x y then
+           idtac
+         else tryif has_evar x then
+             unify x y
+           else tryif has_evar y then
+               unify x y
+             else
+               idtac)
+  end.
+
+Tactic Notation "{" open_constr(old_record) "with" open_constr(new_record) "}" :=
+  let old_record' := eta_expand old_record in
+  partial_unify (old_record = new_record);
+  eexact new_record.
+
+Set Implicit Arguments.
+Record prod A B := pair { fst : A ; snd : B }.
+Infix "*" := prod : type_scope.
+Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
+
+Notation "{ old 'with' new }" := (ltac:({ old with new })) (only parsing).
+
+Check ltac:({ (1, 1) with {| snd := 2 |} }).
+Fail Check { (1, 1) with {| snd := 2 |} }. (* Error: Cannot infer this placeholder of type "Type"; should succeed *)
diff --git a/test-suite/bugs/opened/4755.v b/test-suite/bugs/opened/4755.v
new file mode 100644
index 000000000..9cc0d361e
--- /dev/null
+++ b/test-suite/bugs/opened/4755.v
@@ -0,0 +1,34 @@
+(*I'm not sure which behavior is better.  But if the change is intentional, it should be documented (I don't think it is), and it'd be nice if there were a flag for this, or if -compat 8.4 restored the old behavior.*)
+
+Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms.
+Definition f (v : option nat) := match v with
+                                 | Some k => Some k
+                                 | None => None
+                                 end.
+
+Axioms F G : (option nat -> option nat) -> Prop.
+Axiom FG : forall f, f None = None -> F f = G f.
+
+Axiom admit : forall {T}, T.
+
+Existing Instance eq_Reflexive.
+
+Global Instance foo (A := nat)
+  : Proper ((pointwise_relation _ eq)
+              ==> eq ==> forall_relation (fun _ => Basics.flip Basics.impl))
+           (@option_rect A (fun _ => Prop)) | 0.
+exact admit.
+Qed.
+
+Global Instance bar (A := nat)
+  : Proper ((pointwise_relation _ eq)
+              ==> eq ==> eq ==> Basics.flip Basics.impl)
+           (@option_rect A (fun _ => Prop)) | 0.
+exact admit.
+Qed.
+
+Goal forall k, option_rect (fun _ => Prop) (fun v : nat => v = v /\ F f) True k.
+Proof.
+  intro.
+  pose proof (_ : (Proper (_ ==> eq ==> _) and)).
+  Fail setoid_rewrite (FG _ _); []. (* In 8.5: Error: Tactic failure: Incorrect number of goals (expected 2 tactics); works in 8.4 *)
diff --git a/test-suite/bugs/opened/4771.v b/test-suite/bugs/opened/4771.v
new file mode 100644
index 000000000..396d74bdb
--- /dev/null
+++ b/test-suite/bugs/opened/4771.v
@@ -0,0 +1,22 @@
+Module Type Foo.
+
+Parameter Inline t : nat.
+
+End Foo.
+
+Module F(X : Foo).
+
+Tactic Notation "foo" ref(x) := idtac.
+
+Ltac g := foo X.t.
+
+End F.
+
+Module N.
+Definition t := 0 + 0.
+End N.
+
+Module K := F(N).
+
+(* Was
+Anomaly: Uncaught exception Not_found. Please report. *)
diff --git a/test-suite/bugs/opened/4778.v b/test-suite/bugs/opened/4778.v
new file mode 100644
index 000000000..633d158e9
--- /dev/null
+++ b/test-suite/bugs/opened/4778.v
@@ -0,0 +1,35 @@
+Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms.
+Definition f (v : option nat) := match v with
+                                 | Some k => Some k
+                                 | None => None
+                                 end.
+
+Axioms F G : (option nat -> option nat) -> Prop.
+Axiom FG : forall f, f None = None -> F f = G f.
+
+Axiom admit : forall {T}, T.
+
+Existing Instance eq_Reflexive.
+
+(* This instance is needed in 8.4, but is useless in 8.5 *)
+Global Instance foo (A := nat)
+  : Proper ((pointwise_relation _ eq)
+              ==> eq ==> forall_relation (fun _ => Basics.flip Basics.impl))
+           (@option_rect A (fun _ => Prop)) | 0.
+exact admit.
+Qed.
+
+(*
+(* This is required in 8.5, but useless in 8.4 *)
+Global Instance bar (A := nat)
+  : Proper ((pointwise_relation _ eq)
+              ==> eq ==> eq ==> Basics.flip Basics.impl)
+           (@option_rect A (fun _ => Prop)) | 0.
+exact admit.
+Qed.
+*)
+
+Goal forall k, option_rect (fun _ => Prop) (fun v : nat => v = v /\ F f) True k. Proof.
+  intro.
+  pose proof (_ : (Proper (_ ==> eq ==> _) and)).
+  Fail setoid_rewrite (FG _ _); [ | reflexivity.. ]. (* this should succeed without [Fail], as it does in 8.4 *)
diff --git a/test-suite/bugs/opened/4781.v b/test-suite/bugs/opened/4781.v
new file mode 100644
index 000000000..8b651ac22
--- /dev/null
+++ b/test-suite/bugs/opened/4781.v
@@ -0,0 +1,94 @@
+Ltac force_clear :=
+  clear;
+  repeat match goal with
+         | [ H : _ |- _ ] => clear H
+         | [ H := _ |- _ ] => clearbody H
+         end.
+
+Class abstract_term {T} (x : T) := by_abstract_term : T.
+Hint Extern 0 (@abstract_term ?T ?x) => force_clear; change T; abstract (exact x) : typeclass_instances.
+
+Goal True.
+(* These work: *)
+  let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  pose x.
+  let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let x := (eval cbv iota in (let v : T := x in v)) in
+  pose x.
+  let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let x := match constr:(Set) with ?y => constr:(y) end in
+  pose x.
+(* This fails with an error: *)
+  Fail let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let x := match constr:(x) with ?y => constr:(y) end in
+  pose x. (* The command has indeed failed with message:
+Error: Variable y should be bound to a term. *)
+(* And the rest fail with Anomaly: Uncaught exception Not_found. Please report. *)
+  Fail let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let x := match constr:(x) with ?y => y end in
+  pose x.
+  Fail let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let x := (eval cbv iota in x) in
+  pose x.
+  Fail let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let x := type of x in
+  pose x. (* should succeed *)
+  Fail let term := constr:(I) in
+  let T := type of term in
+  let x := constr:(_ : abstract_term term) in
+  let x := type of x in
+  pose x. (* should succeed *)
+
+(*Apparently what [cbv iota] doesn't see can't hurt it, and [pose] is perfectly happy with abstracted lemmas only some of the time.
+
+Even stranger, consider:*)
+  let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let y := (eval cbv iota in (let v : T := x in v)) in
+  pose y;
+    let x' := fresh "x'" in
+    pose x as x'.
+      let x := (eval cbv delta [x'] in x') in
+      pose x;
+      let z := (eval cbv iota in x) in
+      pose z.
+
+(*This works fine.  But if I change the period to a semicolon, I get:*)
+
+      Fail let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let y := (eval cbv iota in (let v : T := x in v)) in
+  pose y;
+    let x' := fresh "x'" in
+    pose x as x';
+      let x := (eval cbv delta [x'] in x') in
+      pose x. (* Anomaly: Uncaught exception Not_found. Please report. *)
+ (* should succeed *)
+(*and if I use the second one instead of [pose x] (note that using [idtac] works fine), I get:*)
+
+ Fail  let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let y := (eval cbv iota in (let v : T := x in v)) in
+  pose y;
+    let x' := fresh "x'" in
+    pose x as x';
+      let x := (eval cbv delta [x'] in x') in
+      let z := (eval cbv iota in x) in (* Error: Variable x should be bound to a term. *)
+      idtac. (* should succeed *)