From d7a9fea94772971a52d04f9f266fe6d5e25cd40e Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 2 May 2016 15:42:10 +0200
Subject: Avoid infinite loop/stack overflow when using "simpl nomatch" (bug
 #4576).

When encountering a "simpl nomatch" constant, the reduction machinery tries
to unfold it. If the subsequent partial reduction does not produce any
match construct, it keeps going from the reduced term. Unfortunately, the
reduced term has been refolded in the meantime, which means that some of
the previous reduction steps have been canceled, thus causing an infinite
loop. This patch delays the refolding till the very end, so that reduction
always progresses.

Disclaimer: I have no idea what I am doing here. The patch compiles the
standard library and the test suite properly, so hopefully they contain
enough tests to exercise the reduction machinery.
---
 test-suite/bugs/closed/4576.v | 3 +++
 1 file changed, 3 insertions(+)
 create mode 100644 test-suite/bugs/closed/4576.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4576.v b/test-suite/bugs/closed/4576.v
new file mode 100644
index 0000000000..2c643ea779
--- /dev/null
+++ b/test-suite/bugs/closed/4576.v
@@ -0,0 +1,3 @@
+Definition foo := O.
+Arguments foo : simpl nomatch.
+Timeout 1 Eval cbn in id foo.
-- 
cgit v1.2.3


From 857e9ff0a7927d370c8a16e723385a9b199de872 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 2 May 2016 16:54:38 +0200
Subject: Properly handle notations containing spaces (bug #4538).

When a notation was starting or ending a space, Coq assumed the notation
had no terminal symbol in either places. Coq also considered a notation
containing only spaces to be productive. As stated in the documentation,
extraneous spaces are only meant as printing hints, they are not meant to
have any influence on parsing.
---
 test-suite/bugs/closed/4538.v | 1 +
 1 file changed, 1 insertion(+)
 create mode 100644 test-suite/bugs/closed/4538.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4538.v b/test-suite/bugs/closed/4538.v
new file mode 100644
index 0000000000..f925aae9e5
--- /dev/null
+++ b/test-suite/bugs/closed/4538.v
@@ -0,0 +1 @@
+Reserved Notation "   (u *)   ".
-- 
cgit v1.2.3


From 24a125b779c0cf6e9b0662e122c74aa80eb1837b Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 3 May 2016 08:21:36 +0200
Subject: Remove extraneous space in coqtop/pg output (bug #4675).

---
 test-suite/output/Intuition.out |  2 +-
 test-suite/output/Naming.out    | 40 ++++++++++++++++++++--------------------
 test-suite/output/Quote.out     | 18 +++++++++---------
 test-suite/output/set.out       |  6 +++---
 test-suite/output/simpl.out     |  6 +++---
 5 files changed, 36 insertions(+), 36 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/Intuition.out b/test-suite/output/Intuition.out
index e99d9fdebc..f2bf25ca65 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 f0d2562e0f..c142d28ebe 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 ca7fc3624b..998eb37cc8 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 4dfd2bc220..4b72d73eb3 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 73888da9a0..526e468f5b 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
-- 
cgit v1.2.3


From f51dca0647b3213eb20a9b004372e5e6182bb29a Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 3 May 2016 11:02:05 +0200
Subject: Call hooks when terminating a definition proof (bug #4663).

Also register properly the kind of definition.
---
 test-suite/bugs/closed/4663.v | 3 +++
 1 file changed, 3 insertions(+)
 create mode 100644 test-suite/bugs/closed/4663.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4663.v b/test-suite/bugs/closed/4663.v
new file mode 100644
index 0000000000..b76619882a
--- /dev/null
+++ b/test-suite/bugs/closed/4663.v
@@ -0,0 +1,3 @@
+Coercion foo (n : nat) : Set.
+Admitted.
+Check (0 : Set).
-- 
cgit v1.2.3


From 443857fe1bbecf089eb40d522a71a014273c5a23 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 3 May 2016 14:06:17 +0200
Subject: Use the canonical name when looking for an eliminator (bug #4670).

Disclaimer: I have no idea what I am doing.
---
 test-suite/bugs/closed/4670.v | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 test-suite/bugs/closed/4670.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4670.v b/test-suite/bugs/closed/4670.v
new file mode 100644
index 0000000000..6113992953
--- /dev/null
+++ b/test-suite/bugs/closed/4670.v
@@ -0,0 +1,7 @@
+Require Import Coq.Vectors.Vector.
+Module Bar.
+  Definition foo A n (l : Vector.t A n) : True.
+  Proof.
+    induction l ; exact I.
+  Defined.
+End Bar.
-- 
cgit v1.2.3


From e7d54d7fe751e21001c6873fc6092b5adc8eb682 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 3 May 2016 14:22:04 +0200
Subject: Fix bug #4292: Unexpected functor objects.

---
 test-suite/bugs/closed/4292.v | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 test-suite/bugs/closed/4292.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4292.v b/test-suite/bugs/closed/4292.v
new file mode 100644
index 0000000000..403e155eaf
--- /dev/null
+++ b/test-suite/bugs/closed/4292.v
@@ -0,0 +1,7 @@
+Module Type S. End S.
+
+Declare Module M : S.
+
+Module Type F (T: S). End F.
+
+Fail Module Type N := F with Module T := M.
-- 
cgit v1.2.3


From 00a13c3c014e2729d17ad8e8191f20586ae3b52b Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 3 May 2016 15:50:13 +0200
Subject: Test file for #4695: Slow Qed.

---
 test-suite/bugs/closed/4695.v | 38 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 38 insertions(+)
 create mode 100644 test-suite/bugs/closed/4695.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4695.v b/test-suite/bugs/closed/4695.v
new file mode 100644
index 0000000000..a42271811d
--- /dev/null
+++ b/test-suite/bugs/closed/4695.v
@@ -0,0 +1,38 @@
+(* 
+The Qed at the end of this file was slow in 8.5 and 8.5pl1 because the kernel
+term comparison after evaluation was done on constants according to their user
+names. The conversion still succeeded because delta applied, but was much
+slower than with a canonical names comparison.
+*)
+
+Module Mod0.
+
+  Fixpoint rec_ t d : nat :=
+    match d with
+    | O => O
+    | S d' =>
+      match t with
+      | true => rec_ t d'
+      | false => rec_ t d'
+      end
+    end.
+
+  Definition depth := 1000.
+
+  Definition rec t := rec_ t depth.
+
+End Mod0.
+
+
+Module Mod1.
+  Module M := Mod0.
+End Mod1.
+
+
+Axiom rec_prop : forall t d n, Mod1.M.rec_ t d = n.
+
+Lemma slow_qed : forall t n,
+    Mod0.rec t = n.
+Proof.
+  intros; unfold Mod0.rec; apply rec_prop.
+Timeout 2 Qed.
-- 
cgit v1.2.3


From b6e796a8ef956fa25bfeba84545f25b2cfb3aaf9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 3 May 2016 15:06:11 +0200
Subject: Fix bug #3825: Universe annotations on notations should pass through
 or be rejected.

---
 test-suite/bugs/closed/3825.v | 16 ++++++++++++++++
 test-suite/bugs/closed/3922.v |  2 +-
 test-suite/bugs/closed/4544.v |  2 +-
 3 files changed, 18 insertions(+), 2 deletions(-)
 create mode 100644 test-suite/bugs/closed/3825.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3825.v b/test-suite/bugs/closed/3825.v
new file mode 100644
index 0000000000..e594b74b62
--- /dev/null
+++ b/test-suite/bugs/closed/3825.v
@@ -0,0 +1,16 @@
+Set Universe Polymorphism.
+Set Printing Universes.
+
+Axiom foo@{i j} : Type@{i} -> Type@{j}.
+
+Notation bar := foo.
+
+Monomorphic Universes i j.
+
+Check bar@{i j}.
+Fail Check bar@{i}.
+
+Notation qux := (nat -> nat).
+
+Fail Check qux@{i}.
+
diff --git a/test-suite/bugs/closed/3922.v b/test-suite/bugs/closed/3922.v
index 5013bc6ac1..d88e8c3325 100644
--- a/test-suite/bugs/closed/3922.v
+++ b/test-suite/bugs/closed/3922.v
@@ -73,7 +73,7 @@ Definition Trunc_ind {n A}
   (P : Trunc n A -> Type) {Pt : forall aa, IsTrunc n (P aa)}
   : (forall a, P (tr a)) -> (forall aa, P aa)
 := (fun f aa => match aa with tr a => fun _ => f a end Pt).
-Definition merely (A : Type@{i}) : hProp@{i} := BuildhProp (Trunc -1 A).
+Definition merely (A : Type@{i}) : hProp := BuildhProp (Trunc -1 A).
 Definition cconst_factors_contr `{Funext}  {X Y : Type} (f : X -> Y)
            (P : Type) `{Pc : X -> Contr P}
            (g : X -> P) (h : P -> Y) (p : h o g == f)
diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v
index d14cc86fc7..048f31ce3d 100644
--- a/test-suite/bugs/closed/4544.v
+++ b/test-suite/bugs/closed/4544.v
@@ -841,7 +841,7 @@ End Truncation_Modalities.
 
 Module Import TrM := Modalities_Theory Truncation_Modalities.
 
-Definition merely (A : Type@{i}) : hProp@{i} := BuildhProp (Trunc -1 A).
+Definition merely (A : Type@{i}) : hProp := BuildhProp (Trunc -1 A).
 
 Notation IsSurjection := (IsConnMap -1).
 
-- 
cgit v1.2.3


From 27689bac62f85c039517cbd003f8ea74cb9b4aa7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 24 Apr 2016 18:22:53 +0200
Subject: In Regular Subst Tactic mode, ensure that the order of hypotheses is
 preserved, which is a source of incompatibilities w.r.t. released 8.5 but
 which looks to me to be the only possible canonical behavior.

This is I believe a better behavior than the Regular Subst Tactic
behavior in the released 8.5 and 8.5pl1. There, the order of
hypotheses in which substitutions happened was respected, but their
interleaving with other hypotheses was not respected.

So, I consider this to be a fix to the "Regular Subst Tactic" mode.

Also added a more detailed "specification" of the "Regular" behavior
of "subst" in the reference manual.
---
 test-suite/output/subst.out | 97 +++++++++++++++++++++++++++++++++++++++++++++
 test-suite/output/subst.v   | 48 ++++++++++++++++++++++
 2 files changed, 145 insertions(+)
 create mode 100644 test-suite/output/subst.out
 create mode 100644 test-suite/output/subst.v

(limited to 'test-suite')

diff --git a/test-suite/output/subst.out b/test-suite/output/subst.out
new file mode 100644
index 0000000000..f5768ba441
--- /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 0000000000..e48aa6bb28
--- /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.
+
+
-- 
cgit v1.2.3


From dd7cf3a8086fa8a08a421314caec8543ba62226b Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 4 May 2016 10:36:43 +0200
Subject: Handle primitive projections inside types when extracting (bug
 #4616).

Note that extracting terms containing primitive projections is still
utterly broken, so don't use them.
---
 test-suite/bugs/closed/4616.v | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 test-suite/bugs/closed/4616.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4616.v b/test-suite/bugs/closed/4616.v
new file mode 100644
index 0000000000..c862f82067
--- /dev/null
+++ b/test-suite/bugs/closed/4616.v
@@ -0,0 +1,4 @@
+Set Primitive Projections.
+Record Foo' := Foo { foo : Type }.
+Axiom f : forall t : Foo', foo t.
+Extraction f.
-- 
cgit v1.2.3


From 796859aca4fc85dc721b670d95b0c2aaace55e32 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 4 May 2016 11:15:37 +0200
Subject: Fixing subst.out after changing spacing in goal output (24a125b77).

---
 test-suite/output/subst.out | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/subst.out b/test-suite/output/subst.out
index f5768ba441..209b2bc26f 100644
--- a/test-suite/output/subst.out
+++ b/test-suite/output/subst.out
@@ -10,7 +10,7 @@
   HB : True
   H4 : z = 4
   ============================
-   True
+  True
 1 subgoal
   
   x, z : nat
@@ -23,7 +23,7 @@
   HB : True
   H4 : z = 4
   ============================
-   True
+  True
 1 subgoal
   
   x, y : nat
@@ -36,7 +36,7 @@
   HB : True
   H4 : 0 = 4
   ============================
-   True
+  True
 1 subgoal
   
   H1 : 0 = 1
@@ -46,7 +46,7 @@
   HB : True
   H4 : 0 = 4
   ============================
-   True
+  True
 1 subgoal
   
   y, z : nat
@@ -59,7 +59,7 @@
   H1 : 0 = 1
   H2 : 0 = 2
   ============================
-   True
+  True
 1 subgoal
   
   x, z : nat
@@ -72,7 +72,7 @@
   H4 : z = 4
   H3 : 0 = 3
   ============================
-   True
+  True
 1 subgoal
   
   x, y : nat
@@ -85,7 +85,7 @@
   HB : True
   H4 : 0 = 4
   ============================
-   True
+  True
 1 subgoal
   
   HA, HB : True
@@ -94,4 +94,4 @@
   H1 : 0 = 1
   H2 : 0 = 2
   ============================
-   True
+  True
-- 
cgit v1.2.3