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

1 files changed, 4 insertions, 4 deletions

diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 27def8cc13..88e62e46df 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -46,15 +46,15 @@ let pr_open_subgoals () =
 *)
 
 let pr_proof_instr instr = 
-  Util.anomaly "Cannot print a proof_instr"
+  Errors.anomaly "Cannot print a proof_instr"
     (* arnaud: Il nous faut quelque chose de type extr_genarg_printer si on veut aller
                      dans cette direction
        Ppdecl_proof.pr_proof_instr (Global.env()) instr
     *)
 let pr_raw_proof_instr instr =
-  Util.anomaly "Cannot print a raw proof_instr"
+  Errors.anomaly "Cannot print a raw proof_instr"
 let pr_glob_proof_instr instr =
-  Util.anomaly "Cannot print a non-interpreted proof_instr"
+  Errors.anomaly "Cannot print a non-interpreted proof_instr"
 
 let interp_proof_instr _ { Evd.it = gl ; sigma = sigma }=
   Decl_interp.interp_proof_instr 
@@ -65,7 +65,7 @@ let interp_proof_instr _ { Evd.it = gl ; sigma = sigma }=
 let vernac_decl_proof () = 
   let pf = Proof_global.give_me_the_proof () in
   if Proof.is_done pf then 
-    Util.error "Nothing left to prove here."
+    Errors.error "Nothing left to prove here."
   else
     Proof.transaction pf begin fun () ->
       Decl_proof_instr.go_to_proof_mode () ;