Remove extraneous space in coqtop/pg output (bug #4675).

5 files changed, 36 insertions, 36 deletions

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