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

38 files changed, 61 insertions, 19 deletions

diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index 5e2284e13..54ffcd653 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -16,6 +16,7 @@ open Evd
 open Environ
 open Nametab
 open Mod_subst
+open Errors
 open Util
 open Pp
 open Libobject
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 3f5b3f1bf..d413bfbcd 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -7,6 +7,8 @@
 (************************************************************************)
 
 open Compat
+open Pp
+open Errors
 open Util
 open Names
 open Nameops
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index f773da0ee..fcfee055c 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -6,7 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
+open Errors
+open Pp
 open Names
 open Term
 open Evd
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index ad33bae1f..95ab968f0 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Pp
 open Term
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 62d774bd7..3be7e7862 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Pp
 open Flags
@@ -273,7 +274,7 @@ let print_path x = !path_printer x
 
 let message_ambig l =
   (str"Ambiguous paths:" ++ spc () ++
-   prlist_with_sep pr_fnl (fun ijp -> print_path ijp) l)
+   prlist_with_sep fnl (fun ijp -> print_path ijp) l)
 
 (* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit
                          coercion,source,target *)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 553c91274..0c340f9ed 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -14,6 +14,8 @@
    Corbineau, Feb 2008 *)
 (* Turned into an abstract compilation unit by Matthieu Sozeau, March 2006 *)
 
+open Pp
+open Errors
 open Util
 open Names
 open Term
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index 5d814b294..f312802a8 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -6,7 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
+open Errors
+open Pp
 open Evd
 open Names
 open Term
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index c194a0f23..b3daad79e 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Univ
 open Names
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 40e3d0f82..0912a3f23 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -6,7 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
+open Errors
+open Pp
 open Names
 open Term
 open Sign
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 04f86e709..8e61cdebb 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Term
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index fba35925c..5faa86cb0 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Pp
 open Names
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 61f503c7d..82205c91f 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
+open Pp
 open Util
 open Names
 open Glob_term
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 5d6ca2cac..b4354d0cc 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Nameops
@@ -761,7 +762,7 @@ let pr_evar_source = function
       spc () ++ print_constr (constr_of_global c)
   | InternalHole -> str "internal placeholder"
   | TomatchTypeParameter (ind,n) ->
-      nth n ++ str " argument of type " ++ print_constr (mkInd ind)
+      pr_nth n ++ str " argument of type " ++ print_constr (mkInd ind)
   | GoalEvar -> str "goal evar"
   | ImpossibleCase -> str "type of impossible pattern-matching clause"
   | MatchingVar _ -> str "matching variable"
@@ -770,7 +771,7 @@ let pr_evar_info evi =
   let phyps =
     try
       let decls = List.combine (evar_context evi) (evar_filter evi) in
-      prlist_with_sep pr_spc pr_decl (List.rev decls)
+      prlist_with_sep spc pr_decl (List.rev decls)
     with Invalid_argument _ -> str "Ill-formed filtered context" in
   let pty = print_constr evi.evar_concl in
   let pb =
@@ -810,7 +811,7 @@ let evar_dependency_closure n sigma =
 let pr_evar_map_t depth sigma =
   let (evars,(uvs,univs)) = sigma.evars in
   let pr_evar_list l =
-    h 0 (prlist_with_sep pr_fnl
+    h 0 (prlist_with_sep fnl
 	   (fun (ev,evi) ->
 	     h 0 (str(string_of_existential ev) ++
                     str"==" ++ pr_evar_info evi)) l) in
@@ -830,7 +831,7 @@ let pr_evar_map_t depth sigma =
   and svs =
     if Univ.UniverseLSet.is_empty uvs then mt ()
     else str"UNIVERSE VARIABLES:"++brk(0,1)++
-      h 0 (prlist_with_sep pr_fnl 
+      h 0 (prlist_with_sep fnl
 	     (fun u -> Univ.pr_uni_level u) (Univ.UniverseLSet.elements uvs))++fnl()
   and cs =
     if Univ.is_initial_universes univs then mt ()
@@ -844,12 +845,12 @@ let print_env_short env =
   let pr_rel_decl (n, b, _) = pr_body n b in
   let nc = List.rev (named_context env) in
   let rc = List.rev (rel_context env) in
-    str "[" ++ prlist_with_sep pr_spc pr_named_decl nc ++ str "]" ++ spc () ++
-    str "[" ++ prlist_with_sep pr_spc pr_rel_decl rc ++ str "]"
+    str "[" ++ pr_sequence pr_named_decl nc ++ str "]" ++ spc () ++
+    str "[" ++ pr_sequence pr_rel_decl rc ++ str "]"
 
 let pr_constraints pbs =
   h 0
-    (prlist_with_sep pr_fnl 
+    (prlist_with_sep fnl
        (fun (pbty,env,t1,t2) ->
 	  print_env_short env ++ spc () ++ str "|-" ++ spc () ++
 	    print_constr t1 ++ spc() ++
@@ -859,7 +860,7 @@ let pr_constraints pbs =
 	    spc() ++ print_constr t2) pbs)
 
 let pr_evar_map_constraints evd =
-  if evd.conv_pbs = [] then mt() 
+  if evd.conv_pbs = [] then mt()
   else pr_constraints evd.conv_pbs++fnl()
 
 let pr_evar_map allevars evd =
@@ -874,4 +875,4 @@ let pr_evar_map allevars evd =
   v 0 (pp_evm ++ cstrs ++ pp_met)
 
 let pr_metaset metas =
-  str "[" ++ prlist_with_sep spc pr_meta (Metaset.elements metas) ++ str "]"
+  str "[" ++ pr_sequence pr_meta (Metaset.elements metas) ++ str "]"
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 55c54f2c6..5e596e0de 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Pp
+open Errors
 open Util
 open Names
 open Term
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index a736e6eec..5922d38dc 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -7,6 +7,8 @@
 (************************************************************************)
 
 (*i*)
+open Errors
+open Pp
 open Util
 open Names
 open Sign
diff --git a/pretyping/glob_term.mli b/pretyping/glob_term.mli
index fcd28eb8f..f13d0bee9 100644
--- a/pretyping/glob_term.mli
+++ b/pretyping/glob_term.mli
@@ -12,7 +12,8 @@
    and notations are done, but coercions, inference of implicit
    arguments and pattern-matching compilation are not. *)
 
-open Util
+open Errors
+open Pp
 open Names
 open Sign
 open Term
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index a09760295..f08b7493c 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -11,6 +11,7 @@
 (* This file builds various inductive schemes *)
 
 open Pp
+open Errors
 open Util
 open Names
 open Libnames
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index da316fd63..cd86b1e67 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Names
 open Univ
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 7a7451187..ac0022c8c 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -8,6 +8,7 @@
 
 (*i*)
 open Pp
+open Errors
 open Util
 open Names
 open Libnames
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index abb6b510d..0d086919a 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -12,6 +12,7 @@
 (* This file is about generating new or fresh names and dealing with
    alpha-renaming *)
 
+open Errors
 open Util
 open Names
 open Term
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 65f342d88..49b63a4b5 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Names
 open Libnames
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 2cf167919..409e405f5 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Compat
+open Errors
 open Util
 open Names
 open Sign
@@ -43,8 +44,8 @@ type pretype_error =
 exception PretypeError of env * Evd.evar_map * pretype_error
 
 let precatchable_exception = function
-  | Util.UserError _ | TypeError _ | PretypeError _
-  | Loc.Exc_located(_,(Util.UserError _ | TypeError _ |
+  | Errors.UserError _ | TypeError _ | PretypeError _
+  | Loc.Exc_located(_,(Errors.UserError _ | TypeError _ |
     Nametab.GlobalizationError _ | PretypeError _)) -> true
   | _ -> false
 
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 3a3dccb4b..43f934520 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Term
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 901936f33..246993f1a 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -23,6 +23,7 @@
 
 open Compat
 open Pp
+open Errors
 open Util
 open Names
 open Sign
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 47b3ec875..cf47d194e 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -23,7 +23,7 @@ open Evarutil
 (** An auxiliary function for searching for fixpoint guard indexes *)
 
 val search_guard :
-    Util.loc -> env -> int list list -> rec_declaration -> int array
+    Pp.loc -> env -> int list list -> rec_declaration -> int array
 
 type typing_constraint = OfType of types option | IsType
 
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index b3be7afd9..e35004ef1 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -13,6 +13,7 @@
 (* This file registers properties of records: projections and
    canonical structures *)
 
+open Errors
 open Util
 open Pp
 open Names
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index bdb47d689..4e6a702e7 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Term
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 502e238b3..5d7c7ec9f 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Term
 open Inductive
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 0ab43e49c..13b2ddcaa 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Nameops
diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml
index 98091087d..2bf15d2f3 100644
--- a/pretyping/term_dnet.ml
+++ b/pretyping/term_dnet.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 (*i*)
+open Errors
 open Util
 open Term
 open Sign
@@ -304,7 +305,7 @@ struct
   let rec pr_term_pattern p =
     (fun pr_t -> function
        | Term t -> pr_t t
-       | Meta m -> str"["++Util.pr_int (Obj.magic m)++str"]"
+       | Meta m -> str"["++Pp.int (Obj.magic m)++str"]"
     ) (pr_dconstr pr_term_pattern) p
 
   let search_pat cpat dpat dn (up,plug) =
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 6371fd3a7..f64625707 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Nameops
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 5448d97c8..68db293b6 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Pp
 open Names
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index d8a09f95c..8fe06539c 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -16,6 +16,7 @@ open Evd
 open Environ
 open Nametab
 open Mod_subst
+open Errors
 open Util
 open Typeclasses_errors
 open Libobject
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index b49eeac4f..3d36168fd 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -16,6 +16,7 @@ open Environ
 open Nametab
 open Mod_subst
 open Topconstr
+open Errors
 open Util
 
 type direction = Forward | Backward
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index ab7bb9dcb..f6de344a9 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -17,6 +17,7 @@ open Nametab
 open Mod_subst
 open Topconstr
 open Compat
+open Pp
 open Util
 open Libnames
 (*i*)
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index 79f0678ff..fd709763d 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -15,7 +15,8 @@ open Environ
 open Nametab
 open Mod_subst
 open Topconstr
-open Util
+open Errors
+open Pp
 open Libnames
 
 type contexts = Parameters | Properties
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index efcdff9dc..9c8c3989e 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Names
 open Term
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e6fa6eecc..48a2c8c42 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Nameops