Merge branch 'v8.5' into v8.6

6 files changed, 186 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/4069.v b/test-suite/bugs/closed/4069.v
index 21b03ce54..61527764e 100644
--- a/test-suite/bugs/closed/4069.v
+++ b/test-suite/bugs/closed/4069.v
@@ -49,3 +49,56 @@ Lemma bar {A} n m (x : A) :
   skipn n (replicate m x) = replicate (m - n) x.
 Proof. intros. f_equal.
 (* 8.5: one goal, n = m - n *)
+Abort.
+
+Variable F : nat -> Set.
+Variable X : forall n, F (n + 1).
+
+Definition sequator{X Y: Set}{eq:X=Y}(x:X) : Y := eq_rec _ _ x _ eq.
+Definition tequator{X Y}{eq:X=Y}(x:X) : Y := eq_rect _ _ x _ eq.
+Polymorphic Definition pequator{X Y}{eq:X=Y}(x:X) : Y := eq_rect _ _ x _ eq.
+
+Goal {n:nat & F (S n)}.
+eexists.
+unshelve eapply (sequator (X _)).
+f_equal. (*behaves*)
+Undo 2.
+unshelve eapply (pequator (X _)).
+f_equal. (*behaves*)
+Undo 2.
+unshelve eapply (tequator (X _)).
+f_equal. (*behaves now *)
+Focus 2. exact 0.
+simpl.
+reflexivity.
+Defined.
+
+(* Part 2: modulo casts introduced by refine due to reductions in goals *)
+
+Goal {n:nat & F (S n)}.
+eexists.
+(*misbehaves, although same goal as above*)
+Set Printing All.
+unshelve refine (sequator (X _)); revgoals.
+2:exact 0. reflexivity.
+Undo 3. 
+unshelve refine (pequator (X _)); revgoals.
+f_equal.
+Undo 2.
+unshelve refine (tequator (X _)); revgoals.
+f_equal.
+Admitted.
+
+Goal @eq Set nat nat.
+congruence.
+Qed.
+
+Goal @eq Type nat nat.
+congruence. 
+Qed.
+
+Variable T : Type.
+
+Goal @eq Type T T.
+congruence.
+Qed.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4684.v b/test-suite/bugs/closed/4684.v
new file mode 100644
index 000000000..9c0bed42c
--- /dev/null
+++ b/test-suite/bugs/closed/4684.v
@@ -0,0 +1,32 @@
+(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5.  If they use*)
+Require Import Coq.Lists.List.
+Require Import Coq.Vectors.Vector.
+Import ListNotations.
+Import VectorNotations.
+Set Implicit Arguments.
+Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T).
+Arguments mynil {_}, _.
+
+Delimit Scope mylist_scope with mylist.
+Bind Scope mylist_scope with mylist.
+Delimit Scope vector_scope with vector.
+
+Notation " [ ] " := mynil (format "[ ]") : mylist_scope.
+Notation " [ x ] " := (mycons x mynil) : mylist_scope.
+Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z mynil) ..)) : mylist_scope.
+
+Check [ ]%mylist : mylist _.
+Check [ ]%list : list _.
+Check []%vector : Vector.t _ _.
+Check [ _ ]%mylist : mylist _.
+Check [ _ ]%list : list _.
+Check [ _ ]%vector : Vector.t _ _.
+Check [ _ ; _ ]%list : list _.
+Check [ _ ; _ ]%vector : Vector.t _ _.
+Check [ _ ; _ ]%mylist : mylist _.
+Check [ _ ; _ ; _ ]%list : list _.
+Check [ _ ; _ ; _ ]%vector : Vector.t _ _.
+Check [ _ ; _ ; _ ]%mylist : mylist _.
+Check [ _ ; _ ; _ ; _ ]%list : list _.
+Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _.
+Check [ _ ; _ ; _ ; _ ]%mylist : mylist _.
diff --git a/test-suite/bugs/closed/4733.v b/test-suite/bugs/closed/4733.v
new file mode 100644
index 000000000..ac0653492
--- /dev/null
+++ b/test-suite/bugs/closed/4733.v
@@ -0,0 +1,52 @@
+(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
+(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5.  If they use*)
+Require Import Coq.Lists.List.
+Require Import Coq.Vectors.Vector.
+Import ListNotations.
+Import VectorNotations.
+Set Implicit Arguments.
+Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T).
+Arguments mynil {_}, _.
+
+Delimit Scope mylist_scope with mylist.
+Bind Scope mylist_scope with mylist.
+Delimit Scope vector_scope with vector.
+
+Notation " [ ] " := mynil (format "[ ]") : mylist_scope.
+Notation " [ x ] " := (mycons x mynil) : mylist_scope.
+Notation " [ x ; .. ; y ] " := (mycons x .. (mycons y mynil) ..) : mylist_scope.
+
+(** All of these should work fine in -compat 8.4 mode, just as they do in Coq 8.4.  There needs to be a way to specify notations above so that all of these [Check]s go through in both 8.4 and 8.5 *)
+Check [ ]%mylist : mylist _.
+Check [ ]%list : list _.
+Check []%vector : Vector.t _ _.
+Check [ _ ]%mylist : mylist _.
+Check [ _ ]%list : list _.
+Check [ _ ]%vector : Vector.t _ _.
+Check [ _ ; _ ]%list : list _.
+Check [ _ ; _ ]%vector : Vector.t _ _.
+Fail Check [ _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *)
+Check [ _ ; _ ; _ ]%list : list _.
+Check [ _ ; _ ; _ ]%vector : Vector.t _ _.
+Fail Check [ _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *)
+Check [ _ ; _ ; _ ; _ ]%list : list _.
+Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _.
+Fail Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *)
+
+Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z mynil) ..)) : mylist_scope.
+(* Now these all work, but not so in 8.4.  If we get the ability to remove notations, and the above fails can be removed, this section can also just be removed. *)
+Check [ ]%mylist : mylist _.
+Check [ ]%list : list _.
+Check []%vector : Vector.t _ _.
+Check [ _ ]%mylist : mylist _.
+Check [ _ ]%list : list _.
+Check [ _ ]%vector : Vector.t _ _.
+Check [ _ ; _ ]%list : list _.
+Check [ _ ; _ ]%vector : Vector.t _ _.
+Check [ _ ; _ ]%mylist : mylist _.
+Check [ _ ; _ ; _ ]%list : list _.
+Check [ _ ; _ ; _ ]%vector : Vector.t _ _.
+Check [ _ ; _ ; _ ]%mylist : mylist _.
+Check [ _ ; _ ; _ ; _ ]%list : list _.
+Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _.
+Check [ _ ; _ ; _ ; _ ]%mylist : mylist _.
diff --git a/test-suite/bugs/opened/4803.v b/test-suite/bugs/opened/4803.v
new file mode 100644
index 000000000..3ca5c095f
--- /dev/null
+++ b/test-suite/bugs/opened/4803.v
@@ -0,0 +1,34 @@
+(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
+(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5.  If they use*)
+Require Import Coq.Lists.List.
+Require Import Coq.Vectors.Vector.
+Import ListNotations.
+Import VectorNotations.
+Set Implicit Arguments.
+Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T).
+Arguments mynil {_}, _.
+
+Delimit Scope mylist_scope with mylist.
+Bind Scope mylist_scope with mylist.
+Delimit Scope vector_scope with vector.
+
+Notation " [ ] " := mynil (format "[ ]") : mylist_scope.
+Notation " [ x ] " := (mycons x mynil) : mylist_scope.
+Notation " [ x ; .. ; y ] " := (mycons x .. (mycons y mynil) ..) : mylist_scope.
+
+(** All of these should work fine in -compat 8.4 mode, just as they do in Coq 8.4.  There needs to be a way to specify notations above so that all of these [Check]s go through in both 8.4 and 8.5 *)
+Check [ ]%mylist : mylist _.
+Check [ ]%list : list _.
+Check []%vector : Vector.t _ _.
+Check [ _ ]%mylist : mylist _.
+Check [ _ ]%list : list _.
+Check [ _ ]%vector : Vector.t _ _.
+Check [ _ ; _ ]%list : list _.
+Check [ _ ; _ ]%vector : Vector.t _ _.
+Fail Check [ _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser; it should be added to Compat/Coq84.v *)
+Check [ _ ; _ ; _ ]%list : list _.
+Check [ _ ; _ ; _ ]%vector : Vector.t _ _.
+Fail Check [ _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *)
+Check [ _ ; _ ; _ ; _ ]%list : list _.
+Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _.
+Fail Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *)
diff --git a/test-suite/csdp.cache b/test-suite/csdp.cache
index 297ac255d..75dd38fde 100644
--- a/test-suite/csdp.cache
+++ b/test-suite/csdp.cache
diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v
index dc0527d82..bbfe5ec42 100644
--- a/test-suite/success/cc.v
+++ b/test-suite/success/cc.v
@@ -136,3 +136,18 @@ Inductive I : nat -> Type := C : I 0 | D : I 0.
 Goal ~C=D.
 congruence.
 Qed.
+
+(* Example by Jonathan Leivant, congruence up to universes *)
+Section JLeivant.
+  Variables S1 S2 : Set.
+
+  Definition T1 : Type := S1.
+  Definition T2 : Type := S2.
+
+  Goal T1 = T1.
+    congruence.
+    Undo.
+    unfold T1.
+    congruence.
+  Qed.
+End JLeivant.