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

26 files changed, 35 insertions, 6 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 8da06f435..86c8f4913 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -10,6 +10,7 @@
    machine, Oct 2004 *)
 (* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *)
 
+open Errors
 open Util
 open Names
 open Cbytecodes
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 143d6eb49..d62ac79bf 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -19,6 +19,7 @@
 (* This file implements a lazy reduction for the Calculus of Inductive
    Constructions *)
 
+open Errors
 open Util
 open Pp
 open Term
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index 92109258d..c195a5496 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -44,7 +44,7 @@ let set_strategy k l =
       cst_opacity :=
       if l=default then Cmap.remove c !cst_opacity
       else Cmap.add c l !cst_opacity
-  | RelKey _ -> Util.error "set_strategy: RelKey"
+  | RelKey _ -> Errors.error "set_strategy: RelKey"
 
 let get_transp_state () =
   (Idmap.fold
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 02330339d..1a405e98b 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -14,6 +14,7 @@
    declarations over global constants and inductive types *)
 
 open Pp
+open Errors
 open Util
 open Names
 open Term
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 1a84b9876..db304e33d 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -21,6 +21,7 @@
    global constants/axioms, mutual inductive definitions and the
    module system *)
 
+open Errors
 open Util
 open Names
 open Univ
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 7a41e62c4..c38d4186f 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -20,6 +20,7 @@
 (* This file defines the type of environments on which the
    type-checker works, together with simple related functions *)
 
+open Errors
 open Util
 open Names
 open Sign
diff --git a/kernel/esubst.ml b/kernel/esubst.ml
index cbce04d62..dad5b1420 100644
--- a/kernel/esubst.ml
+++ b/kernel/esubst.ml
@@ -10,6 +10,7 @@
 
 (* Support for explicit substitutions *)
 
+open Errors
 open Util
 
 (*********************)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 46e866a04..aa5e132c6 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Names
 open Univ
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 21f86233a..b2d924714 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Names
 open Univ
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 314cc0ee0..777f39183 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -14,6 +14,7 @@
    substitution in module constructions *)
 
 open Pp
+open Errors
 open Util
 open Names
 open Term
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index a384c836c..e2304f119 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -12,6 +12,7 @@
 (* This module provides the main functions for type-checking module
    declarations *)
 
+open Errors
 open Util
 open Names
 open Univ
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 0c2c6bd71..a422bae66 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -15,6 +15,7 @@
 
 (* This file provides with various operations on modules and module types *)
 
+open Errors
 open Util
 open Pp
 open Names
diff --git a/kernel/modops.mli b/kernel/modops.mli
index b9c36d5af..9f8a306fa 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Names
 open Univ
diff --git a/kernel/names.ml b/kernel/names.ml
index ae8ad093c..b01d5675b 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -19,12 +19,16 @@
    Élie Soubiran, ... *)
 
 open Pp
+open Errors
 open Util
 
 (** {6 Identifiers } *)
 
 type identifier = string
 
+let check_ident_soft x = Option.iter Pp.warning (ident_refutation x)
+let check_ident x = Option.iter Errors.error (ident_refutation x)
+
 let id_of_string s = check_ident_soft s; String.copy s
 let string_of_id id = String.copy id
 
diff --git a/kernel/names.mli b/kernel/names.mli
index 34c5e62c5..63c64f364 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -10,6 +10,9 @@
 
 type identifier
 
+val check_ident : string -> unit
+val check_ident_soft : string -> unit
+
 (** Parsing and printing of identifiers *)
 val string_of_id : identifier -> string
 val id_of_string : string -> identifier
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 985aac95f..ec4a2d195 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -13,6 +13,7 @@
 
 (* This file defines the type of kernel environments *)
 
+open Errors
 open Util
 open Names
 open Sign
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 40ce887b2..0d279bc39 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Names
 open Sign
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index fc5e32cf5..10eccd059 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -15,6 +15,7 @@
 (* Equal inductive types by Jacek Chrzaszcz as part of the module
    system, Aug 2002 *)
 
+open Errors
 open Util
 open Names
 open Term
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index c2d71ebb2..e87bc9c1c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -57,6 +57,7 @@
    etc.
 *)
 
+open Errors
 open Util
 open Names
 open Univ
diff --git a/kernel/sign.ml b/kernel/sign.ml
index 71169563b..861cb0b6c 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -16,6 +16,7 @@
    names-based contexts *)
 
 open Names
+open Errors
 open Util
 open Term
 
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index c141a02aa..9fb045407 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -12,6 +12,7 @@
 (* This module checks subtyping of module types *)
 
 (*i*)
+open Errors
 open Util
 open Names
 open Univ
@@ -278,7 +279,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
 	      let c2 = Declarations.force lc2 in
 	      check_conv NotConvertibleBodyField cst conv env c1 c2))
    | IndType ((kn,i),mind1) ->
-       ignore (Util.error (
+       ignore (Errors.error (
        "The kernel does not recognize yet that a parameter can be " ^
        "instantiated by an inductive type. Hint: you can rename the " ^
        "inductive type and give a definition to map the old name to the new " ^
@@ -289,7 +290,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
       let typ2 = Typeops.type_of_constant_type env cb2.const_type in
        check_conv NotConvertibleTypeField cst conv_leq env arity1 typ2
    | IndConstr (((kn,i),j) as cstr,mind1) ->
-      ignore (Util.error (
+      ignore (Errors.error (
        "The kernel does not recognize yet that a parameter can be " ^
        "instantiated by a constructor. Hint: you can rename the " ^
        "constructor and give a definition to map the old name to the new " ^
diff --git a/kernel/term.ml b/kernel/term.ml
index dcb63cf7b..0a4782d8c 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -23,6 +23,7 @@
    Inductive Constructions (CIC) terms together with constructors,
    destructors, iterators and basic functions *)
 
+open Errors
 open Util
 open Pp
 open Names
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 478b9c6fc..887a90010 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -12,6 +12,7 @@
 (* This module provides the main entry points for type-checking basic
    declarations *)
 
+open Errors
 open Util
 open Names
 open Univ
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 49106c912..a2dd09976 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Names
 open Univ
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 0193542a3..d967846f1 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -14,6 +14,7 @@
 (* Revisions by Bruno Barras, Hugo Herbelin, Pierre Letouzey *)
 
 open Pp
+open Errors
 open Util
 
 (* Universes are stratified by a partial ordering $\le$.
@@ -817,9 +818,9 @@ let pr_arc = function
   | _, Canonical {univ=u; lt=lt; le=le} ->
       pr_uni_level u ++ str " " ++
       v 0
-        (prlist_with_sep pr_spc (fun v -> str "< " ++ pr_uni_level v) lt ++
+        (pr_sequence (fun v -> str "< " ++ pr_uni_level v) lt ++
 	 (if lt <> [] & le <> [] then spc () else mt()) ++
-         prlist_with_sep pr_spc (fun v -> str "<= " ++ pr_uni_level v) le) ++
+         pr_sequence (fun v -> str "<= " ++ pr_uni_level v) le) ++
       fnl ()
   | u, Equiv v ->
       pr_uni_level u  ++ str " = " ++ pr_uni_level v ++ fnl ()
diff --git a/kernel/vm.ml b/kernel/vm.ml
index 86aed5d93..851b66d48 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -224,7 +224,7 @@ let whd_val : values -> whd =
 	   | 1 -> Vfix(Obj.obj o, None)
 	   | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o))
 	   | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), [])
-	   | _ -> Util.anomaly "Vm.whd : kind_of_closure does not work")
+	   | _ -> Errors.anomaly "Vm.whd : kind_of_closure does not work")
 	else Vconstr_block(Obj.obj o)