Merge branch 'v8.5'

7 files changed, 181 insertions, 36 deletions

diff --git a/test-suite/output/Intuition.out b/test-suite/output/Intuition.out
index e99d9fdeb..f2bf25ca6 100644
--- a/test-suite/output/Intuition.out
+++ b/test-suite/output/Intuition.out
@@ -3,4 +3,4 @@
   m, n : Z
   H : (m >= n)%Z
   ============================
-   (m >= m)%Z
+  (m >= m)%Z
diff --git a/test-suite/output/Naming.out b/test-suite/output/Naming.out
index f0d2562e0..c142d28eb 100644
--- a/test-suite/output/Naming.out
+++ b/test-suite/output/Naming.out
@@ -2,40 +2,40 @@
   
   x3 : nat
   ============================
-   forall x x1 x4 x0 : nat,
-   (forall x2 x5 : nat, x2 + x1 = x4 + x5) -> x + x1 = x4 + x0
+  forall x x1 x4 x0 : nat,
+  (forall x2 x5 : nat, x2 + x1 = x4 + x5) -> x + x1 = x4 + x0
 1 subgoal
   
   x3, x, x1, x4, x0 : nat
   H : forall x x3 : nat, x + x1 = x4 + x3
   ============================
-   x + x1 = x4 + x0
+  x + x1 = x4 + x0
 1 subgoal
   
   x3 : nat
   ============================
-   forall x x1 x4 x0 : nat,
-   (forall x2 x5 : nat, x2 + x1 = x4 + x5 -> foo (S x2 + x1)) ->
-   x + x1 = x4 + x0 -> foo (S x)
+  forall x x1 x4 x0 : nat,
+  (forall x2 x5 : nat, x2 + x1 = x4 + x5 -> foo (S x2 + x1)) ->
+  x + x1 = x4 + x0 -> foo (S x)
 1 subgoal
   
   x3 : nat
   ============================
-   forall x x1 x4 x0 : nat,
-   (forall x2 x5 : nat,
-    x2 + x1 = x4 + x5 ->
-    forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) ->
-   x + x1 = x4 + x0 ->
-   forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
+  forall x x1 x4 x0 : nat,
+  (forall x2 x5 : nat,
+   x2 + x1 = x4 + x5 ->
+   forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) ->
+  x + x1 = x4 + x0 ->
+  forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
 1 subgoal
   
   x3, x, x1, x4, x0 : nat
   ============================
-   (forall x2 x5 : nat,
-    x2 + x1 = x4 + x5 ->
-    forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) ->
-   x + x1 = x4 + x0 ->
-   forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
+  (forall x2 x5 : nat,
+   x2 + x1 = x4 + x5 ->
+   forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) ->
+  x + x1 = x4 + x0 ->
+  forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
 1 subgoal
   
   x3, x, x1, x4, x0 : nat
@@ -44,7 +44,7 @@
       forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (S x + x1)
   H0 : x + x1 = x4 + x0
   ============================
-   forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
+  forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
 1 subgoal
   
   x3, x, x1, x4, x0 : nat
@@ -54,10 +54,10 @@
   H0 : x + x1 = x4 + x0
   x5, x6, x7, S : nat
   ============================
-   x5 + S = x6 + x7 + Datatypes.S x
+  x5 + S = x6 + x7 + Datatypes.S x
 1 subgoal
   
   x3, a : nat
   H : a = 0 -> forall a : nat, a = 0
   ============================
-   a = 0
+  a = 0
diff --git a/test-suite/output/Quote.out b/test-suite/output/Quote.out
index ca7fc3624..998eb37cc 100644
--- a/test-suite/output/Quote.out
+++ b/test-suite/output/Quote.out
@@ -8,17 +8,17 @@
   H : interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_atom End_idx) \/
       B
   ============================
-   interp_f
-     (Node_vm B (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (Empty_vm Prop))
-     (f_and (f_atom (Left_idx End_idx))
-        (f_and (f_or (f_atom End_idx) (f_atom (Left_idx End_idx)))
-           (f_or (f_atom (Left_idx End_idx)) (f_not (f_atom End_idx)))))
+  interp_f
+    (Node_vm B (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (Empty_vm Prop))
+    (f_and (f_atom (Left_idx End_idx))
+       (f_and (f_or (f_atom End_idx) (f_atom (Left_idx End_idx)))
+          (f_or (f_atom (Left_idx End_idx)) (f_not (f_atom End_idx)))))
 1 subgoal
   
   H : interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_atom End_idx) \/
       B
   ============================
-   interp_f (Node_vm B (Empty_vm Prop) (Empty_vm Prop))
-     (f_and (f_const A)
-        (f_and (f_or (f_atom End_idx) (f_const A))
-           (f_or (f_const A) (f_not (f_atom End_idx)))))
+  interp_f (Node_vm B (Empty_vm Prop) (Empty_vm Prop))
+    (f_and (f_const A)
+       (f_and (f_or (f_atom End_idx) (f_const A))
+          (f_or (f_const A) (f_not (f_atom End_idx)))))
diff --git a/test-suite/output/set.out b/test-suite/output/set.out
index 4dfd2bc22..4b72d73eb 100644
--- a/test-suite/output/set.out
+++ b/test-suite/output/set.out
@@ -3,16 +3,16 @@
   y1 := 0 : nat
   x := 0 + 0 : nat
   ============================
-   x = x
+  x = x
 1 subgoal
   
   y1, y2 := 0 : nat
   x := y2 + 0 : nat
   ============================
-   x = x
+  x = x
 1 subgoal
   
   y1, y2, y3 := 0 : nat
   x := y2 + y3 : nat
   ============================
-   x = x
+  x = x
diff --git a/test-suite/output/simpl.out b/test-suite/output/simpl.out
index 73888da9a..526e468f5 100644
--- a/test-suite/output/simpl.out
+++ b/test-suite/output/simpl.out
@@ -2,14 +2,14 @@
   
   x : nat
   ============================
-   x = S x
+  x = S x
 1 subgoal
   
   x : nat
   ============================
-   0 + x = S x
+  0 + x = S x
 1 subgoal
   
   x : nat
   ============================
-   x = 1 + x
+  x = 1 + x
diff --git a/test-suite/output/subst.out b/test-suite/output/subst.out
new file mode 100644
index 000000000..209b2bc26
--- /dev/null
+++ b/test-suite/output/subst.out
@@ -0,0 +1,97 @@
+1 subgoal
+  
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  H1 : 0 = 1
+  HA : True
+  H2 : 0 = 2
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  ============================
+  True
+1 subgoal
+  
+  x, z : nat
+  Hx : x = 0
+  Hz : z = 0
+  H1 : x = 1
+  HA : True
+  H2 : x = 2
+  H3 : 0 = 3
+  HB : True
+  H4 : z = 4
+  ============================
+  True
+1 subgoal
+  
+  x, y : nat
+  Hx : x = 0
+  Hy : y = 0
+  H1 : x = 1
+  HA : True
+  H2 : x = 2
+  H3 : y = 3
+  HB : True
+  H4 : 0 = 4
+  ============================
+  True
+1 subgoal
+  
+  H1 : 0 = 1
+  HA : True
+  H2 : 0 = 2
+  H3 : 0 = 3
+  HB : True
+  H4 : 0 = 4
+  ============================
+  True
+1 subgoal
+  
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  HA : True
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  H1 : 0 = 1
+  H2 : 0 = 2
+  ============================
+  True
+1 subgoal
+  
+  x, z : nat
+  Hx : x = 0
+  Hz : z = 0
+  H1 : x = 1
+  HA : True
+  H2 : x = 2
+  HB : True
+  H4 : z = 4
+  H3 : 0 = 3
+  ============================
+  True
+1 subgoal
+  
+  x, y : nat
+  Hx : x = 0
+  Hy : y = 0
+  H1 : x = 1
+  HA : True
+  H2 : x = 2
+  H3 : y = 3
+  HB : True
+  H4 : 0 = 4
+  ============================
+  True
+1 subgoal
+  
+  HA, HB : True
+  H4 : 0 = 4
+  H3 : 0 = 3
+  H1 : 0 = 1
+  H2 : 0 = 2
+  ============================
+  True
diff --git a/test-suite/output/subst.v b/test-suite/output/subst.v
new file mode 100644
index 000000000..e48aa6bb2
--- /dev/null
+++ b/test-suite/output/subst.v
@@ -0,0 +1,48 @@
+(* Ensure order of hypotheses is respected after "subst" *)
+
+Set Regular Subst Tactic.
+Goal forall x y z, x = 0 -> y = 0 -> z = 0 -> x = 1 -> True -> x = 2 -> y = 3 -> True -> z = 4 -> True.
+intros * Hx Hy Hz H1 HA H2 H3 HB H4.
+(* From now on, the order after subst is consistently H1, HA, H2, H3, HB, H4 *)
+subst x.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, H3, HB, H4, H1, H2 *)
+Show.
+Undo.
+subst y.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, HB, H4, H3 *)
+Show.
+Undo.
+subst z.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, H3, HB, H4 *)
+Show.
+Undo.
+subst.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, HB, H4, H3, H1, H2 *)
+(* In 8.5pl0 and 8.5pl1 with regular subst tactic mode, the order was HA, HB, H1, H2, H3, H4 *)
+Show.
+trivial.
+Qed.
+
+Unset Regular Subst Tactic.
+Goal forall x y z, x = 0 -> y = 0 -> z = 0 -> x = 1 -> True -> x = 2 -> y = 3 -> True -> z = 4 -> True.
+intros * Hx Hy Hz H1 HA H2 H3 HB H4.
+subst x.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, H3, HB, H4, H1, H2 *)
+Show.
+Undo.
+subst y.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, HB, H4, H3 *)
+Show.
+Undo.
+subst z.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, H3, HB, H4 *)
+Show.
+Undo.
+subst.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, HB, H4, H3, H1, H2 *)
+(* In 8.5pl0 and 8.5pl1 with regular subst tactic mode, the order was HA, HB, H1, H2, H3, H4 *)
+Show.
+trivial.
+Qed.
+
+