17 files changed, 98 insertions, 64 deletions
diff --git a/test-suite/bugs/closed/2850.v b/test-suite/bugs/closed/2850.v
deleted file mode 100644
index 64a93aeb00..0000000000
--- a/test-suite/bugs/closed/2850.v
+++ /dev/null
@@ -1,2 +0,0 @@
-Definition id {A} (x : A) := x.
-Fail Compute id.
diff --git a/test-suite/bugs/closed/4785.v b/test-suite/bugs/closed/4785.v
index c3c97d3f59..0d347b262d 100644
--- a/test-suite/bugs/closed/4785.v
+++ b/test-suite/bugs/closed/4785.v
@@ -1,5 +1,4 @@
 Require Coq.Lists.List Coq.Vectors.Vector.
-Require Coq.Compat.Coq85.
 
 Module A.
 Import Coq.Lists.List Coq.Vectors.Vector.
@@ -21,12 +20,10 @@ Delimit Scope mylist_scope with mylist.
 Bind Scope mylist_scope with mylist.
 Arguments mynil {_}, _.
 Arguments mycons {_} _ _.
-Notation " [] " := mynil (compat "8.5") : mylist_scope.
 Notation " [ ] " := mynil (format "[ ]") : mylist_scope.
 Notation " [ x ] " := (mycons x nil) : mylist_scope.
 Notation " [ x ; y ; .. ; z ] " :=  (mycons x (mycons y .. (mycons z nil) ..)) : mylist_scope.
 
-Import Coq.Compat.Coq85.
 Locate Module VectorNotations.
 Import VectorDef.VectorNotations.
 
@@ -35,11 +32,3 @@ Check []%mylist : mylist _.
 Check [ ]%mylist : mylist _.
 Check [ ]%list : list _.
 End A.
-
-Module B.
-Import Coq.Compat.Coq85.
-
-Goal True.
-  idtac; []. (* Check that importing the compat file doesn't break the [ | .. | ] syntax of Ltac *)
-Abort.
-End B.
diff --git a/test-suite/bugs/closed/4785_compat_85.v b/test-suite/bugs/closed/4785_compat_85.v
deleted file mode 100644
index bbb34f465c..0000000000
--- a/test-suite/bugs/closed/4785_compat_85.v
+++ /dev/null
@@ -1,46 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.5") -*- *)
-Require Coq.Lists.List Coq.Vectors.Vector.
-Require Coq.Compat.Coq85.
-
-Module A.
-Import Coq.Lists.List Coq.Vectors.Vector.
-Import ListNotations.
-Check [ ]%list : list _.
-Import VectorNotations ListNotations.
-Delimit Scope vector_scope with vector.
-Check [ ]%vector : Vector.t _ _.
-Check []%vector : Vector.t _ _.
-Check [ ]%list : list _.
-Fail Check []%list : list _.
-
-Goal True.
-  idtac; [ ]. (* Note that vector notations break the [ | .. | ] syntax of Ltac *)
-Abort.
-
-Inductive mylist A := mynil | mycons (x : A) (xs : mylist A).
-Delimit Scope mylist_scope with mylist.
-Bind Scope mylist_scope with mylist.
-Arguments mynil {_}, _.
-Arguments mycons {_} _ _.
-Notation " [] " := mynil (compat "8.5") : mylist_scope.
-Notation " [ ] " := mynil (format "[ ]") : mylist_scope.
-Notation " [ x ] " := (mycons x nil) : mylist_scope.
-Notation " [ x ; y ; .. ; z ] " :=  (mycons x (mycons y .. (mycons z nil) ..)) : mylist_scope.
-
-Import Coq.Compat.Coq85.
-Locate Module VectorNotations.
-Import VectorDef.VectorNotations.
-
-Check []%vector : Vector.t _ _.
-Check []%mylist : mylist _.
-Check [ ]%mylist : mylist _.
-Check [ ]%list : list _.
-End A.
-
-Module B.
-Import Coq.Compat.Coq85.
-
-Goal True.
-  idtac; []. (* Check that importing the compat file doesn't break the [ | .. | ] syntax of Ltac *)
-Abort.
-End B.
diff --git a/test-suite/bugs/closed/4798.v b/test-suite/bugs/closed/4798.v
index dbc3d46fce..6f2bcb9685 100644
--- a/test-suite/bugs/closed/4798.v
+++ b/test-suite/bugs/closed/4798.v
@@ -1,3 +1,3 @@
 Check match 2 with 0 => 0 | S n => n end.
-Notation "|" := 1 (compat "8.4").
+Notation "|" := 1 (compat "8.6").
 Check match 2 with 0 => 0 | S n => n end. (* fails *)
diff --git a/test-suite/bugs/closed/4873.v b/test-suite/bugs/closed/4873.v
index 3be36d8475..39299883ad 100644
--- a/test-suite/bugs/closed/4873.v
+++ b/test-suite/bugs/closed/4873.v
@@ -1,6 +1,5 @@
 Require Import Coq.Classes.Morphisms.
 Require Import Relation_Definitions.
-Require Import Coq.Compat.Coq85.
 
 Fixpoint tuple' T n : Type :=
   match n with
diff --git a/test-suite/bugs/closed/6878.v b/test-suite/bugs/closed/6878.v
new file mode 100644
index 0000000000..70f1b3127a
--- /dev/null
+++ b/test-suite/bugs/closed/6878.v
@@ -0,0 +1,8 @@
+
+Set Universe Polymorphism.
+Module Type T.
+  Axiom foo : Prop.
+End T.
+
+(** Used to anomaly *)
+Fail Module M : T with Definition foo := Type.
diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh
index 2439d3f378..aa6b0a9a43 100755
--- a/test-suite/coq-makefile/timing/run.sh
+++ b/test-suite/coq-makefile/timing/run.sh
@@ -38,9 +38,29 @@ make print-pretty-timed-diff TIMING_SORT_BY=diff || exit $?
 INFINITY="∞"
 INFINITY_REPLACEMENT="+.%" # assume that if the before time is zero, we expected the time to increase
 
+TO_SED_IN_BOTH=(
+    -e s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" # Whether or not something shows up as ∞ depends on whether a time registers as 0.s or as 0.001s, so we can't rely on this being consistent
+    -e s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" # Whether or not something shows up as N/A depends on whether a time registers as 0.s or as 0.001s, so we can't rely on this being consistent
+    -e s'/ *$//g' # the number of trailing spaces depends on how many digits percentages end up being; since this varies across runs, we remove trailing spaces
+    -e s'/[0-9]*\.[0-9]*//g' # the precise timing numbers vary, so we strip them out
+    -e s'/^-*$/------/g' # When none of the numbers get over 100 (or 1000, in per-file), the width of the table is different, so we normalize the number of dashes for table separators
+)
+
+TO_SED_IN_PER_FILE=(
+    -e s'/[0-9]//g' # unclear whether this is actually needed above and beyond s'/[0-9]*\.[0-9]*//g'; it's been here from the start
+    -e s'/  */ /g' # unclear whether this is actually needed for per-file timing; it's been here from the start
+    -e s'/\(Total.*\)-\(.*\)-/\1+\2+/g' # Overall time in the per-file timing diff should be around 0; if it comes out negative, we remove the sign
+)
+
+TO_SED_IN_PER_LINE=(
+    -e s'/0//g' # unclear whether this is actually needed above and beyond s'/[0-9]*\.[0-9]*//g'; it's been here from the start
+    -e s'/  */ /g' # Sometimes 0 will show up as 0m00.s, sometimes it'll end up being more like 0m00.001s; we must strip out the spaces that result from left-aligning numbers of different widths based on how many digits Coq's [-time] gives
+    -e s'/+/-/g' # some code lines don't really change, but this can show up as either -0m00.01s or +0m00.01s, so we need to normalize the signs
+    )
+
 for ext in "" .desired; do
     for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do
-        cat ${file}${ext} | grep -v 'warning: undefined variable' | sed s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" | sed s'/[0-9]//g' | sed s'/ *$//g' | sed s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" | sed s'/^-*$/------/g' | sed s'/  */ /g' | sed s'/\(Total.*\)-\(.*\)-/\1+\2+/g' > ${file}${ext}.processed
+        cat ${file}${ext} | grep -v 'warning: undefined variable' | sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_FILE[@]}" > ${file}${ext}.processed
     done
 done
 for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do
@@ -74,7 +94,7 @@ echo
 
 for ext in "" .desired; do
     for file in A.v.timing.diff; do
-        cat ${file}${ext} | sed s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" | sed s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" | sed s'/[0-9]*\.[0-9]*//g' | sed s'/0//g' | sed s'/  */ /g' | sed s'/ *$//g' | sed s'/+/-/g' | sort > ${file}${ext}.processed
+        cat ${file}${ext} | sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_LINE[@]}" | sort > ${file}${ext}.processed
     done
 done
 for file in A.v.timing.diff; do
diff --git a/test-suite/output/Load.out b/test-suite/output/Load.out
new file mode 100644
index 0000000000..0904d5540b
--- /dev/null
+++ b/test-suite/output/Load.out
@@ -0,0 +1,6 @@
+f = 2
+     : nat
+u = I
+     : True
+The command has indeed failed with message:
+Files processed by Load cannot leave open proofs.
diff --git a/test-suite/output/Load.v b/test-suite/output/Load.v
new file mode 100644
index 0000000000..967507415a
--- /dev/null
+++ b/test-suite/output/Load.v
@@ -0,0 +1,7 @@
+Load "output/load/Load_noproof.v".
+Print f.
+
+Load "output/load/Load_proof.v".
+Print u.
+
+Fail Load "output/load/Load_openproof.v".
diff --git a/test-suite/output/PrintInfos.v b/test-suite/output/PrintInfos.v
index 08918981a4..a498db3e89 100644
--- a/test-suite/output/PrintInfos.v
+++ b/test-suite/output/PrintInfos.v
@@ -26,6 +26,7 @@ About bar.
 Print bar.
 
 About Peano. (* Module *)
+Set Warnings "-deprecated".
 About existS2. (* Notation *)
 
 Arguments eq_refl {A} {x}, {A} x.
diff --git a/test-suite/output/bug6821.out b/test-suite/output/bug6821.out
new file mode 100644
index 0000000000..7b12b53200
--- /dev/null
+++ b/test-suite/output/bug6821.out
@@ -0,0 +1,2 @@
+forall f : nat -> Type, f x where x : nat := 1
+     : Type
diff --git a/test-suite/output/bug6821.v b/test-suite/output/bug6821.v
new file mode 100644
index 0000000000..40627e331e
--- /dev/null
+++ b/test-suite/output/bug6821.v
@@ -0,0 +1,8 @@
+(* Was failing at printing time with stack overflow due to an infinite
+   eta-expansion *)
+
+Notation "x 'where' y .. z := v " :=
+  ((fun y => .. ((fun z => x) v) ..) v)
+  (at level 11, v at next level, y binder, z binder).
+
+Check forall f, f x where x := 1.
diff --git a/test-suite/output/load/Load_noproof.v b/test-suite/output/load/Load_noproof.v
new file mode 100644
index 0000000000..aaf1ffe26d
--- /dev/null
+++ b/test-suite/output/load/Load_noproof.v
@@ -0,0 +1 @@
+Definition f := 2.
diff --git a/test-suite/output/load/Load_openproof.v b/test-suite/output/load/Load_openproof.v
new file mode 100644
index 0000000000..204d4ecbfe
--- /dev/null
+++ b/test-suite/output/load/Load_openproof.v
@@ -0,0 +1 @@
+Lemma k : True.
diff --git a/test-suite/output/load/Load_proof.v b/test-suite/output/load/Load_proof.v
new file mode 100644
index 0000000000..e47f66a193
--- /dev/null
+++ b/test-suite/output/load/Load_proof.v
@@ -0,0 +1,2 @@
+Lemma u : True.
+Proof. exact I. Qed.
diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v
index 62249666b3..448d0082db 100644
--- a/test-suite/success/rewrite.v
+++ b/test-suite/success/rewrite.v
@@ -151,10 +151,25 @@ Abort.
 
 (* Check that rewriting within evars still work (was broken in 8.5beta1) *)
 
-
 Goal forall (a: unit) (H: a = tt), exists x y:nat, x = y.
 intros; eexists; eexists.
 rewrite H.
 Undo.
 subst.
 Abort.
+
+(* Check that iterated rewriting does not rewrite in the side conditions *)
+(* Example from Sigurd Schneider, extracted from contrib containers *)
+
+Lemma EQ
+  : forall (e e' : nat), True -> e = e'.
+Admitted.
+
+Lemma test (v1 v2 v3: nat) (v' : v1 = v2) : v2 = v1.
+Proof.
+  rewrite <- (EQ v1 v2) in *.
+  exact v'.
+  (* There should be only two side conditions *)
+  exact I.
+  exact I.
+Qed.
diff --git a/test-suite/success/vm_evars.v b/test-suite/success/vm_evars.v
new file mode 100644
index 0000000000..2c8b099ef0
--- /dev/null
+++ b/test-suite/success/vm_evars.v
@@ -0,0 +1,23 @@
+Fixpoint iter {A} (n : nat) (f : A -> A) (x : A) :=
+match n with
+| 0 => x
+| S n => iter n f (f x)
+end.
+
+Goal nat -> True.
+Proof.
+intros n.
+evar (f : nat -> nat).
+cut (iter 10 f 0 = 0).
+vm_compute.
+intros; constructor.
+instantiate (f := (fun x => x)).
+reflexivity.
+Qed.
+
+Goal exists x, x = 5 + 5.
+Proof.
+  eexists.
+  vm_compute.
+  reflexivity.
+Qed.