Noise for nothing

Util only depends on Ocaml stdlib and Utf8 tables.
Generic pretty printing and loc functions are in Pp.
Generic errors are in Errors.

+ Training white-spaces, useless open, prlist copies random erasure.
Too many "open Errors" on the contrary.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 16 insertions, 17 deletions

diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index 7c9b1e27cf..f5636fbf9d 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -22,16 +22,15 @@ Expands to: Constant Coq.Init.Peano.minus
 minus : nat -> nat -> nat
 
 Argument scopes are [nat_scope nat_scope]
-The simpl tactic unfolds minus
-  when the 1st and 2nd arguments evaluate to a constructor and
-  when applied to 2 arguments 
+The simpl tactic unfolds minus when the 1st and
+  2nd arguments evaluate to a constructor and when applied to 2 arguments 
 minus is transparent
 Expands to: Constant Coq.Init.Peano.minus
 minus : nat -> nat -> nat
 
 Argument scopes are [nat_scope nat_scope]
-The simpl tactic unfolds minus
-  when the 1st and 2nd arguments evaluate to a constructor 
+The simpl tactic unfolds minus when the 1st and
+  2nd arguments evaluate to a constructor 
 minus is transparent
 Expands to: Constant Coq.Init.Peano.minus
 pf :
@@ -65,30 +64,30 @@ Expands to: Constant Top.S1.S2.f
 f : T1 -> T2 -> nat -> unit -> nat -> nat
 
 Argument scopes are [_ _ nat_scope _ nat_scope]
-The simpl tactic unfolds f
-  when the 3rd, 4th and 5th arguments evaluate to a constructor 
+The simpl tactic unfolds f when the 3rd, 4th and
+  5th arguments evaluate to a constructor 
 f is transparent
 Expands to: Constant Top.S1.S2.f
 f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
 Argument T2 is implicit
 Argument scopes are [type_scope _ _ nat_scope _ nat_scope]
-The simpl tactic unfolds f
-  when the 4th, 5th and 6th arguments evaluate to a constructor 
+The simpl tactic unfolds f when the 4th, 5th and
+  6th arguments evaluate to a constructor 
 f is transparent
 Expands to: Constant Top.S1.f
 f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
 Arguments T1, T2 are implicit
 Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope]
-The simpl tactic unfolds f
-  when the 5th, 6th and 7th arguments evaluate to a constructor 
+The simpl tactic unfolds f when the 5th, 6th and
+  7th arguments evaluate to a constructor 
 f is transparent
 Expands to: Constant Top.f
 f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
-The simpl tactic unfolds f
-  when the 5th, 6th and 7th arguments evaluate to a constructor 
+The simpl tactic unfolds f when the 5th, 6th and
+  7th arguments evaluate to a constructor 
 f is transparent
 Expands to: Constant Top.f
 forall w : r, w 3 true = tt
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index e443115cb3..20042a5ed0 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -53,8 +53,8 @@ myplus : forall T : Type, T -> nat -> nat -> nat
 Arguments are renamed to Z, t, n, m
 Argument Z is implicit and maximally inserted
 Argument scopes are [type_scope _ nat_scope nat_scope]
-The simpl tactic unfolds myplus
-  when the 2nd and 3rd arguments evaluate to a constructor 
+The simpl tactic unfolds myplus when the 2nd and
+  3rd arguments evaluate to a constructor 
 myplus is transparent
 Expands to: Constant Top.Test1.myplus
 myplus
@@ -90,8 +90,8 @@ myplus : forall T : Type, T -> nat -> nat -> nat
 Arguments are renamed to Z, t, n, m
 Argument Z is implicit and maximally inserted
 Argument scopes are [type_scope _ nat_scope nat_scope]
-The simpl tactic unfolds myplus
-  when the 2nd and 3rd arguments evaluate to a constructor 
+The simpl tactic unfolds myplus when the 2nd and
+  3rd arguments evaluate to a constructor 
 myplus is transparent
 Expands to: Constant Top.myplus
 myplus