From 401f17afa2e9cc3f2d734aef0d71a2c363838ebd Mon Sep 17 00:00:00 2001
From: pboutill
Date: Fri, 2 Mar 2012 22:30:29 +0000
Subject: 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
---
 plugins/decl_mode/decl_expr.mli       | 2 +-
 plugins/decl_mode/decl_interp.ml      | 1 +
 plugins/decl_mode/decl_mode.ml        | 1 +
 plugins/decl_mode/decl_proof_instr.ml | 1 +
 plugins/decl_mode/g_decl_mode.ml4     | 8 ++++----
 plugins/decl_mode/ppdecl_proof.ml     | 1 +
 6 files changed, 9 insertions(+), 5 deletions(-)

(limited to 'plugins/decl_mode')

diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli
index fa6acaeb1f..e84864f966 100644
--- a/plugins/decl_mode/decl_expr.mli
+++ b/plugins/decl_mode/decl_expr.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Util
+open Pp
 open Tacexpr
 
 type 'it statement =
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index b3e076c49b..512269e559 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Names
 open Topconstr
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
index af6aa4bf59..5f9563cb21 100644
--- a/plugins/decl_mode/decl_mode.ml
+++ b/plugins/decl_mode/decl_mode.ml
@@ -9,6 +9,7 @@
 open Names
 open Term
 open Evd
+open Errors
 open Util
 
 
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index c1553b35db..e3a95fb4fa 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Pp
 open Evd
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 () ;
diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml
index b866efaba4..a2e078ee2d 100644
--- a/plugins/decl_mode/ppdecl_proof.ml
+++ b/plugins/decl_mode/ppdecl_proof.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Pp
 open Decl_expr
-- 
cgit v1.2.3