Merge branch 'v8.6'

14 files changed, 316 insertions, 2 deletions

diff --git a/test-suite/bugs/closed/3690.v b/test-suite/bugs/closed/3690.v
index c24173abf1..fd9640b890 100644
--- a/test-suite/bugs/closed/3690.v
+++ b/test-suite/bugs/closed/3690.v
@@ -47,7 +47,7 @@ Type@{Top.21} -> Type@{Top.23}
               Top.23 < Top.22
                *) *)
 Fail Check @qux@{Set Set}.
-Fail Check @qux@{Set Set Set}.
+Check @qux@{Type Type Type Type}.
 (* [qux] should only need two universes *)
-Check @qux@{i j k}.  (* Error: The command has not failed!, but I think this is suboptimal *)
+Check @qux@{i j k l}.  (* Error: The command has not failed!, but I think this is suboptimal *)
 Fail Check @qux@{i j}.
diff --git a/test-suite/bugs/closed/4069.v b/test-suite/bugs/closed/4069.v
index 21b03ce541..61527764e2 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/4622.v b/test-suite/bugs/closed/4622.v
new file mode 100644
index 0000000000..ffa478cb87
--- /dev/null
+++ b/test-suite/bugs/closed/4622.v
@@ -0,0 +1,24 @@
+Set Primitive Projections.
+
+Record foo : Type := bar { x : unit }.
+
+Goal forall t u, bar t = bar u -> t = u.
+Proof.
+  intros.
+  injection H.
+  trivial.
+Qed.
+(* Was: Error: Pattern-matching expression on an object of inductive type foo has invalid information. *)
+
+(** Dependent pattern-matching is ok on this one as it has eta *)
+Definition baz (x : foo) :=
+  match x as x' return x' = x' with
+  | bar u => eq_refl
+  end.
+
+Inductive foo' : Type := bar' {x' : unit; y: foo'}.
+(** Dependent pattern-matching is not ok on this one *)
+Fail Definition baz' (x : foo') :=
+  match x as x' return x' = x' with
+  | bar' u y => eq_refl
+  end.
diff --git a/test-suite/bugs/closed/4684.v b/test-suite/bugs/closed/4684.v
new file mode 100644
index 0000000000..9c0bed42c4
--- /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 0000000000..ac0653492a
--- /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/closed/4858.v b/test-suite/bugs/closed/4858.v
new file mode 100644
index 0000000000..a2fa93832a
--- /dev/null
+++ b/test-suite/bugs/closed/4858.v
@@ -0,0 +1,7 @@
+Require Import Nsatz.
+Goal True.
+try nsatz_compute
+ (PEc 0%Z :: PEc (-1)%Z
+    :: PEpow (PEsub (PEX Z 2) (PEX Z 3)) 1
+       :: PEsub (PEX Z 1) (PEX Z 1) :: nil).
+Abort.
diff --git a/test-suite/bugs/closed/4873.v b/test-suite/bugs/closed/4873.v
new file mode 100644
index 0000000000..f2f917b4e7
--- /dev/null
+++ b/test-suite/bugs/closed/4873.v
@@ -0,0 +1,72 @@
+Require Import Coq.Classes.Morphisms.
+Require Import Relation_Definitions.
+Require Import Coq.Compat.Coq85.
+
+Fixpoint tuple' T n : Type :=
+  match n with
+  | O => T
+  | S n' => (tuple' T n' * T)%type
+  end.
+
+Definition tuple T n : Type :=
+  match n with
+  | O => unit
+  | S n' => tuple' T n'
+  end.
+
+Fixpoint to_list' {T} (n:nat) {struct n} : tuple' T n -> list T :=
+  match n with
+  | 0 => fun x => (x::nil)%list
+  | S n' => fun xs : tuple' T (S n') => let (xs', x) := xs in (x :: to_list' n' xs')%list
+  end.
+
+Definition to_list {T} (n:nat) : tuple T n -> list T :=
+  match n with
+  | 0 => fun _ => nil
+  | S n' => fun xs : tuple T (S n') => to_list' n' xs
+  end.
+
+Program Fixpoint from_list' {T} (y:T) (n:nat) (xs:list T) : length xs = n -> tuple' T n :=
+  match n return _ with
+  | 0 =>
+    match xs return (length xs = 0 -> tuple' T 0) with
+    | nil => fun _ => y
+    | _ => _ (* impossible *)
+    end
+  | S n' =>
+    match xs return (length xs = S n' -> tuple' T (S n')) with
+    | cons x xs' => fun _ => (from_list' x n' xs' _, y)
+    | _ => _ (* impossible *)
+    end
+  end.
+Goal True.
+  pose from_list'_obligation_3 as e.
+  repeat (let e' := fresh in
+          rename e into e';
+          (pose (e' nat) as e || pose (e' 0) as e || pose (e' nil) as e || pose (e' eq_refl) as e);
+          subst e').
+  progress hnf in e.
+  pose (eq_refl : e = eq_refl).
+  exact I.
+Qed.
+
+Program Definition from_list {T} (n:nat) (xs:list T) : length xs = n -> tuple T n :=
+match n return _ with
+| 0 =>
+    match xs return (length xs = 0 -> tuple T 0) with
+    | nil => fun _ : 0 = 0 => tt
+    | _ => _ (* impossible *)
+    end
+| S n' =>
+    match xs return (length xs = S n' -> tuple T (S n')) with
+    | cons x xs' => fun _ => from_list' x n' xs' _
+    | _ => _ (* impossible *)
+    end
+end.
+
+Lemma to_list_from_list : forall {T} (n:nat) (xs:list T) pf, to_list n (from_list n xs pf) = xs.
+Proof.
+  destruct xs; simpl; intros; subst; auto.
+  generalize dependent t. simpl in *.
+  induction xs; simpl in *; intros; congruence.
+Qed.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4880.v b/test-suite/bugs/closed/4880.v
new file mode 100644
index 0000000000..5569798d54
--- /dev/null
+++ b/test-suite/bugs/closed/4880.v
@@ -0,0 +1,11 @@
+Require Import Coq.Reals.Reals Coq.nsatz.Nsatz.
+Local Open Scope R.
+
+Goal forall x y : R,
+  x*x =  y *  y ->
+  x*x = -y * -y ->
+  x*(x*x) = 0 -> (* The associativity does not actually matter, *)
+  (x*x)*x = 0.   (* just otherwise [assumption] would solve the goal. *)
+Proof.
+  nsatz.
+Qed.
diff --git a/test-suite/bugs/opened/4803.v b/test-suite/bugs/opened/4803.v
new file mode 100644
index 0000000000..3ca5c095f5
--- /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 297ac255d3..8e5708cf02 100644
--- a/test-suite/csdp.cache
+++ b/test-suite/csdp.cache
diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out
index 6354ad469e..62e9ef4b20 100644
--- a/test-suite/output/Errors.out
+++ b/test-suite/output/Errors.out
@@ -5,3 +5,6 @@ Unable to unify "nat" with "True".
 The command has indeed failed with message:
 In nested Ltac calls to "f" and "apply x", last call failed.
 Unable to unify "nat" with "True".
+The command has indeed failed with message:
+Ltac call to "instantiate" failed.
+Error: Instance is not well-typed in the environment of ?x.
diff --git a/test-suite/output/Errors.v b/test-suite/output/Errors.v
index 352c87385f..424d24801c 100644
--- a/test-suite/output/Errors.v
+++ b/test-suite/output/Errors.v
@@ -16,3 +16,12 @@ Goal True.
 Fail simpl; apply 0.
 Fail simpl; f 0.
 Abort.
+
+(* Test instantiate error messages *)
+
+Goal forall T1 (P1 : T1 -> Type), sigT P1 -> sigT P1.
+intros T1 P1 H1.
+eexists ?[x].
+destruct H1 as [x1 H1].
+Fail instantiate (x:=projT1 x1).
+Abort.
diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v
index dc0527d826..bbfe5ec420 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.
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index b5e6ccd618..2fa7704941 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -47,7 +47,9 @@ Check _.(next) : option Y.
 Lemma eta_ind (y : Y) : y = Build_Y y.(next).
 Proof. Fail reflexivity. Abort.
 
+Inductive Fdef := { Fa : nat ; Fb := Fa; Fc : Fdef }.
 
+Fail Scheme Fdef_rec := Induction for Fdef Sort Prop.
 
 (* 
   Rules for parsing and printing of primitive projections and their eta expansions.