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

89 files changed, 173 insertions, 103 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index e3d27f719..7434f5e8a 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -9,6 +9,7 @@
 (* This file implements the basic congruence-closure algorithm by *)
 (* Downey,Sethi and Tarjan. *)
 
+open Errors
 open Util
 open Pp
 open Goptions
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index 78dbee3fe..d530495f8 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Term
 open Names
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index bb1d50c99..4c8c80ba4 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -9,6 +9,7 @@
 (* This file uses the (non-compressed) union-find structure to generate *)
 (* proof-trees that will be transformed into proof-terms in cctac.ml4   *)
 
+open Errors
 open Util
 open Names
 open Term
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index ec31f8917..0a3697e2a 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -26,6 +26,7 @@ open Ccalgo
 open Tacinterp
 open Ccproof
 open Pp
+open Errors
 open Util
 open Format
 
@@ -410,7 +411,7 @@ let cc_tactic depth additionnal_terms gls=
 		       begin
 			 str "\"congruence with (" ++
 			 prlist_with_sep
-			   (fun () -> str ")" ++ pr_spc () ++ str "(")
+			   (fun () -> str ")" ++ spc () ++ str "(")
 			   (Termops.print_constr_env (pf_env gls))
 			   terms_to_complete ++
 			 str ")\","
diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli
index fa6acaeb1..e84864f96 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 b3e076c49..512269e55 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 af6aa4bf5..5f9563cb2 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 c1553b35d..e3a95fb4f 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 27def8cc1..88e62e46d 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 b866efaba..a2e078ee2 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
diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml
index 837195e44..fd96b6d1c 100644
--- a/plugins/dp/dp.ml
+++ b/plugins/dp/dp.ml
@@ -11,6 +11,7 @@
      Zenon)
 *)
 
+open Errors
 open Util
 open Pp
 open Libobject
diff --git a/plugins/dp/dp_zenon.mll b/plugins/dp/dp_zenon.mll
index 949e91e34..1e82034c0 100644
--- a/plugins/dp/dp_zenon.mll
+++ b/plugins/dp/dp_zenon.mll
@@ -3,7 +3,7 @@
 
   open Lexing
   open Pp
-  open Util
+  open Errors
   open Names
   open Tacmach
   open Dp_why
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 0bd5b8434..1b443f753 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Term
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 73062328b..7c517dd9b 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -11,6 +11,7 @@ open Declarations
 open Names
 open Libnames
 open Pp
+open Errors
 open Util
 open Miniml
 open Table
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 219b3913f..d9ee92c05 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 (*i*)
+open Errors
 open Util
 open Names
 open Term
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 96731ed27..fe249cd65 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -9,6 +9,7 @@
 (*s Production of Haskell syntax. *)
 
 open Pp
+open Errors
 open Util
 open Names
 open Nameops
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index 5a19cc3f5..a5b57a474 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -9,6 +9,7 @@
 (*s Target language for extraction: a core ML called MiniML. *)
 
 open Pp
+open Errors
 open Util
 open Names
 open Libnames
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index c244e046d..f03170948 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -8,6 +8,7 @@
 
 (*i*)
 open Pp
+open Errors
 open Util
 open Names
 open Libnames
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index 029e8cf46..630db6f06 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Names
 open Term
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 9e8dd8286..123edd4c3 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -10,6 +10,7 @@ open Names
 open Declarations
 open Environ
 open Libnames
+open Errors
 open Util
 open Miniml
 open Table
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index ed69ec457..d99bca6f4 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -9,6 +9,7 @@
 (*s Production of Ocaml syntax. *)
 
 open Pp
+open Errors
 open Util
 open Names
 open Nameops
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 215076555..157788ece 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -9,6 +9,7 @@
 (*s Production of Scheme syntax. *)
 
 open Pp
+open Errors
 open Util
 open Names
 open Nameops
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 238befd25..667182480 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -15,6 +15,7 @@ open Summary
 open Libobject
 open Goptions
 open Libnames
+open Errors
 open Util
 open Pp
 open Miniml
@@ -337,7 +338,7 @@ let warning_both_mod_and_cst q mp r =
 
 let error_axiom_scheme r i =
   err (str "The type scheme axiom " ++ spc () ++
-       safe_pr_global r ++ spc () ++ str "needs " ++ pr_int i ++
+       safe_pr_global r ++ spc () ++ str "needs " ++ int i ++
        str " type variable(s).")
 
 let check_inside_module () =
diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4
index 9e4f4d745..15c495ae7 100644
--- a/plugins/field/field.ml4
+++ b/plugins/field/field.ml4
@@ -15,6 +15,7 @@ open Tacinterp
 open Tacmach
 open Term
 open Typing
+open Errors
 open Util
 open Vernacinterp
 open Vernacexpr
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index d67dceeac..566b2b8b0 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -12,6 +12,7 @@ open Term
 open Termops
 open Reductionops
 open Tacmach
+open Errors
 open Util
 open Declarations
 open Libnames
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 4a38c48dc..f5b16e43f 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -17,7 +17,6 @@ open Tacticals
 open Tacinterp
 open Term
 open Names
-open Util
 open Libnames
 
 (* declaring search depth as a global option *)
@@ -103,6 +102,7 @@ let normalize_evaluables=
 	   unfold_in_hyp (Lazy.force defined_connectives)
 	   (Tacexpr.InHypType id)) *)
 
+open Pp
 open Genarg
 open Ppconstr
 open Printer
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 16831d3ec..8d4b0eee1 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -10,6 +10,8 @@ open Formula
 open Sequent
 open Unify
 open Rules
+open Pp
+open Errors
 open Util
 open Term
 open Glob_term
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 23eeb2f66..b56fe4e50 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Names
 open Term
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index f75678c60..780e3f3e7 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Term
+open Errors
 open Util
 open Formula
 open Unify
@@ -235,7 +236,7 @@ let print_cmap map=
   let print_entry c l s=
     let xc=Constrextern.extern_constr false (Global.env ()) c in
       str "| " ++
-      Util.prlist Printer.pr_global l ++
+      prlist Printer.pr_global l ++
       str " : " ++
       Ppconstr.pr_constr_expr xc ++
       cut () ++
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index c5c2bb954..5587e9fbb 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Term
+open Errors
 open Util
 open Formula
 open Tacmach
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 299a0054a..48c402cc0 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Formula
 open Tacmach
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 484937858..1a629aac9 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -503,11 +503,11 @@ let rec fourier gl=
 		        with _ -> ())
               hyps;
     (* lineq = les inéquations découlant des hypothèses *)
-    if !lineq=[] then Util.error "No inequalities";
+    if !lineq=[] then Errors.error "No inequalities";
     let res=fourier_lineq (!lineq) in
     let tac=ref tclIDTAC in
     if res=[]
-    then Util.error "fourier failed"
+    then Errors.error "fourier failed"
     (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *)
     else (match res with
         [(cres,sres,lc)]->
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 865074d6b..13b3dabdf 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1,4 +1,5 @@
 open Printer
+open Errors
 open Util
 open Term
 open Namegen
@@ -1048,7 +1049,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
 		{finfos with
 		   equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with
 					      ConstRef c -> c
-					    | _ -> Util.anomaly "Not a constant"
+					    | _ -> Errors.anomaly "Not a constant"
 					 )
 		}
 	  | _ -> ()
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 6df9d574f..0f776ee6e 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -1,4 +1,5 @@
 open Printer
+open Errors
 open Util
 open Term
 open Namegen
@@ -304,7 +305,7 @@ let defined () =
     Lemmas.save_named false
   with
     | UserError("extract_proof",msg) ->
-	Util.errorlabstrm
+	Errors.errorlabstrm
 	  "defined"
 	  ((try
 	      str "On goal : " ++ fnl () ++  pr_open_subgoals () ++ fnl ()
@@ -659,9 +660,9 @@ let build_scheme fas =
 	      try
 		match Nametab.global f with
 		  | Libnames.ConstRef c -> c
-		  | _ -> Util.error "Functional Scheme can only be used with functions"
+		  | _ -> Errors.error "Functional Scheme can only be used with functions"
 	      with Not_found ->
-	      	Util.error ("Cannot find "^ Libnames.string_of_reference f)
+	      	Errors.error ("Cannot find "^ Libnames.string_of_reference f)
 	    in
 	    (f_as_constant,sort)
 	 )
@@ -692,7 +693,7 @@ let build_case_scheme fa =
   let funs =  (fun (_,f,_) ->
 		 try Libnames.constr_of_global (Nametab.global f)
 		 with Not_found ->
-		   Util.error ("Cannot find "^ Libnames.string_of_reference f)) fa in
+		   Errors.error ("Cannot find "^ Libnames.string_of_reference f)) fa in
   let first_fun = destConst  funs in
 
   let funs_mp,funs_dp,_ = Names.repr_con first_fun in
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 123399d56..f330f9ff9 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -25,10 +25,10 @@ let pr_binding prc = function
 let pr_bindings prc prlc = function
   | Glob_term.ImplicitBindings l ->
       brk (1,1) ++ str "with" ++ brk (1,1) ++
-      Util.prlist_with_sep spc prc l
+      pr_sequence prc l
   | Glob_term.ExplicitBindings l ->
       brk (1,1) ++ str "with" ++ brk (1,1) ++
-        Util.prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
+        pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
   | Glob_term.NoBindings -> mt ()
 
 let pr_with_bindings prc prlc (c,bl) =
@@ -111,7 +111,7 @@ TACTIC EXTEND snewfunind
 END
 
 
-let pr_constr_coma_sequence prc _ _ = Util.prlist_with_sep Util.pr_comma prc
+let pr_constr_coma_sequence prc _ _ = prlist_with_sep pr_comma prc
 
 ARGUMENT EXTEND constr_coma_sequence'
   TYPED AS constr_list
@@ -180,12 +180,12 @@ let warning_error names e =
     | Building_graph e ->
 	Pp.msg_warning
 	  (str "Cannot define graph(s) for " ++
-	     h 1 (prlist_with_sep (fun _ -> str","++spc ()) Libnames.pr_reference names) ++
+	     h 1 (pr_enum Libnames.pr_reference names) ++
 	     if do_observe () then (spc () ++ Errors.print e) else mt ())
     | Defining_principle e ->
 	Pp.msg_warning
 	  (str "Cannot define principle(s) for "++
-	     h 1 (prlist_with_sep (fun _ -> str","++spc ()) Libnames.pr_reference names) ++
+	     h 1 (pr_enum Libnames.pr_reference names) ++
 	     if do_observe () then Errors.print e else mt ())
     | _ -> raise e
 
@@ -207,7 +207,7 @@ VERNAC COMMAND EXTEND NewFunctionalScheme
 		    ;
 		    try Functional_principles_types.build_scheme fas
 		    with Functional_principles_types.No_graph_found ->
-		      Util.error ("Cannot generate induction principle(s)")
+		      Errors.error ("Cannot generate induction principle(s)")
     		      | e ->
 			  let names = List.map (fun (_,na,_) -> na) fas in
 			  warning_error names e
@@ -377,7 +377,7 @@ let finduction (oid:identifier option) (heuristic: fapp_info list -> fapp_info l
   let info_list = find_fapp test g in
   let ordered_info_list = heuristic info_list in
   prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) ordered_info_list);
-  if List.length ordered_info_list = 0 then Util.error "function not found in goal\n";
+  if List.length ordered_info_list = 0 then Errors.error "function not found in goal\n";
   let taclist: Proof_type.tactic list =
     List.map
       (fun info ->
@@ -419,7 +419,7 @@ TACTIC EXTEND finduction
     ["finduction" ident(id) natural_opt(oi)] ->
       [
 	match oi with
-	  | Some(n) when n<=0 -> Util.error "numerical argument must be > 0"
+	  | Some(n) when n<=0 -> Errors.error "numerical argument must be > 0"
 	  | _ ->
 	      let heuristic = chose_heuristic oi in
 	      finduction (Some id) heuristic tclIDTAC
@@ -458,19 +458,19 @@ VERNAC COMMAND EXTEND MergeFunind
       "with" "(" ident(id2) ne_ident_list(cl2)  ")" "using" ident(id) ] ->
      [
        let f1 = Constrintern.interp_constr Evd.empty (Global.env())
-	 (CRef (Libnames.Ident (Util.dummy_loc,id1))) in
+	 (CRef (Libnames.Ident (Pp.dummy_loc,id1))) in
        let f2 = Constrintern.interp_constr Evd.empty (Global.env())
-	 (CRef (Libnames.Ident (Util.dummy_loc,id2))) in
+	 (CRef (Libnames.Ident (Pp.dummy_loc,id2))) in
        let f1type = Typing.type_of (Global.env()) Evd.empty f1 in
        let f2type = Typing.type_of (Global.env()) Evd.empty f2 in
        let ar1 = List.length (fst (decompose_prod f1type)) in
        let ar2 = List.length (fst (decompose_prod f2type)) in
        let _ =
 	 if ar1 <> List.length cl1 then
-	   Util.error ("not the right number of arguments for " ^ string_of_id id1) in
+	   Errors.error ("not the right number of arguments for " ^ string_of_id id1) in
        let _ =
 	 if ar2 <> List.length cl2 then
-	   Util.error ("not the right number of arguments for " ^ string_of_id id2) in
+	   Errors.error ("not the right number of arguments for " ^ string_of_id id2) in
        Merge.merge id1 id2 (Array.of_list cl1) (Array.of_list cl2)  id
      ]
 END
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index c88c66693..6a5888874 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -5,6 +5,7 @@ open Term
 open Glob_term
 open Libnames
 open Indfun_common
+open Errors
 open Util
 open Glob_termops
 
@@ -977,8 +978,8 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		      ((Util.list_chop nparam args'))
 		    in
 		    let rt_typ =
-		       GApp(Util.dummy_loc,
-			    GRef (Util.dummy_loc,Libnames.IndRef ind),
+		       GApp(Pp.dummy_loc,
+			    GRef (Pp.dummy_loc,Libnames.IndRef ind),
 			    (List.map
 			      (fun p -> Detyping.detype false []
 				 (Termops.names_of_rel_context env)
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index cdd0eaf71..b458346d4 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -1,5 +1,6 @@
 open Pp
 open Glob_term
+open Errors
 open Util
 open Names
 (* Ocaml 3.06 Map.S does not handle is_empty *)
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index bfd153579..80a8811f1 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -84,9 +84,9 @@ val alpha_rt : Names.identifier list -> glob_constr -> glob_constr
 
 (* same as alpha_rt but for case branches *)
 val alpha_br : Names.identifier list ->
-    Util.loc * Names.identifier list * Glob_term.cases_pattern list *
+    Pp.loc * Names.identifier list * Glob_term.cases_pattern list *
     Glob_term.glob_constr ->
-    Util.loc * Names.identifier list * Glob_term.cases_pattern list *
+    Pp.loc * Names.identifier list * Glob_term.cases_pattern list *
     Glob_term.glob_constr
 
 
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 97a49d6f0..449dcd20e 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -1,3 +1,4 @@
+open Errors
 open Util
 open Names
 open Term
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index e65b58086..faa5f2e46 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -1,3 +1,4 @@
+open Errors
 open Util
 open Names
 open Term
@@ -17,7 +18,7 @@ val functional_induction :
   bool ->
   Term.constr ->
   (Term.constr * Term.constr Glob_term.bindings) option ->
-  Genarg.intro_pattern_expr Util.located option ->
+  Genarg.intro_pattern_expr Pp.located option ->
   Proof_type.goal Tacmach.sigma -> Proof_type.goal list Evd.sigma
 
 
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index d6fb28ba5..60aa99b12 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -54,7 +54,7 @@ let locate_with_msg msg f x =
   try
     f x
   with
-    | Not_found -> raise (Util.UserError("", msg))
+    | Not_found -> raise (Errors.UserError("", msg))
     | e -> raise e
 
 
@@ -79,7 +79,7 @@ let chop_rlambda_n  =
 	  | Glob_term.GLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b
 	  | Glob_term.GLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b
 	  | _ ->
-	      raise (Util.UserError("chop_rlambda_n",
+	      raise (Errors.UserError("chop_rlambda_n",
 				    str "chop_rlambda_n: Not enough Lambdas"))
   in
   chop_lambda_n []
@@ -91,7 +91,7 @@ let chop_rprod_n  =
       else
 	match rt with
 	  | Glob_term.GProd(_,name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b
-	  | _ -> raise (Util.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products"))
+	  | _ -> raise (Errors.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products"))
   in
   chop_prod_n []
 
@@ -112,10 +112,10 @@ let list_add_set_eq eq_fun x l =
 
 let const_of_id id =
   let _,princ_ref =
-    qualid_of_reference (Libnames.Ident (Util.dummy_loc,id))
+    qualid_of_reference (Libnames.Ident (Pp.dummy_loc,id))
   in
   try Nametab.locate_constant princ_ref
-  with Not_found -> Util.error ("cannot find "^ string_of_id id)
+  with Not_found -> Errors.error ("cannot find "^ string_of_id id)
 
 let def_of_const t =
    match (Term.kind_of_term t) with
@@ -361,7 +361,7 @@ let pr_info f_info =
 
 let pr_table tb =
   let l = Cmap.fold (fun k v acc -> v::acc) tb [] in
-  Util.prlist_with_sep fnl pr_info l
+  Pp.prlist_with_sep fnl pr_info l
 
 let in_Function : function_info -> Libobject.obj =
   Libobject.declare_object
@@ -397,7 +397,7 @@ let _ =
 
 let find_or_none id =
   try Some
-    (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> Util.anomaly "Not a constant"
+    (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> Errors.anomaly "Not a constant"
     )
   with Not_found -> None
 
@@ -425,7 +425,7 @@ let add_Function is_general f =
   and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind")
   and graph_ind =
     match Nametab.locate (qualid_of_ident (mk_rel_id f_id))
-    with | IndRef ind -> ind | _ -> Util.anomaly "Not an inductive"
+    with | IndRef ind -> ind | _ -> Errors.anomaly "Not an inductive"
   in
   let finfos =
     { function_constant = f;
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 9835ad605..a9b162819 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 open Tacexpr
 open Declarations
+open Errors
 open Util
 open Names
 open Term
@@ -29,10 +30,10 @@ let pr_binding prc  =
 let pr_bindings prc prlc = function
   | Glob_term.ImplicitBindings l ->
       brk (1,1) ++ str "with" ++ brk (1,1) ++
-      Util.prlist_with_sep spc prc l
+      pr_sequence prc l
   | Glob_term.ExplicitBindings l ->
       brk (1,1) ++ str "with" ++ brk (1,1) ++
-        Util.prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
+        pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
   | Glob_term.NoBindings -> mt ()
 
 
@@ -1142,7 +1143,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 
       mk_correct_id f_id
     in
-     ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,first_lemma_id) with _ -> ());
+     ignore(try Vernacentries.vernac_reset_name (Pp.dummy_loc,first_lemma_id) with _ -> ());
     raise e
 
 
@@ -1239,7 +1240,7 @@ let invfun qhyp f  =
   let f =
     match f with
       | ConstRef f -> f
-      | _ -> raise (Util.UserError("",str "Not a function"))
+      | _ -> raise (Errors.UserError("",str "Not a function"))
   in
   try
     let finfos = find_Function_infos f in
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 4eedf8dc2..3b3f3057b 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -11,6 +11,7 @@
 open Libnames
 open Tactics
 open Indfun_common
+open Errors
 open Util
 open Topconstr
 open Vernacexpr
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 5e0aac4c2..c37de6e4a 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -17,6 +17,7 @@ open Pp
 open Names
 open Libnames
 open Nameops
+open Errors
 open Util
 open Closure
 open RedFlags
@@ -1273,7 +1274,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
   let sign = initialize_named_context_for_proof () in
   let na = next_global_ident_away name [] in
   if Termops.occur_existential gls_type then
-    Util.error "\"abstract\" cannot handle existentials";
+    Errors.error "\"abstract\" cannot handle existentials";
   let hook _ _ =
     let opacity =
       let na_ref = Libnames.Ident (dummy_loc,na) in
@@ -1553,7 +1554,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
       hook 
   with e ->
     begin
-      ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ());
+      ignore(try Vernacentries.vernac_reset_name (Pp.dummy_loc,functional_id) with _ -> ());
 (*       anomaly "Cannot create termination Lemma" *)
       raise e
     end
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index 3b6b69879..9deeb6066 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -20,7 +20,7 @@ open Quote
 open Ring
 open Mutils
 open Glob_term
-open Util
+open Errors
 
 let out_arg = function
   | ArgVar _ -> anomaly "Unevaluated or_var variable"
diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4
index a317307e0..c6d23afa6 100644
--- a/plugins/nsatz/nsatz.ml4
+++ b/plugins/nsatz/nsatz.ml4
@@ -9,6 +9,7 @@
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
 open Pp
+open Errors
 open Util
 open Names
 open Term
diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml
index 45fcb2d25..b940ab89d 100644
--- a/plugins/nsatz/polynom.ml
+++ b/plugins/nsatz/polynom.ml
@@ -8,6 +8,7 @@
 
 (* Recursive polynomials: R[x1]...[xn]. *)
 open Utile
+open Errors
 open Util
 
 (* 1. Coefficients: R *)
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index d7dfe1491..1057c646f 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -13,6 +13,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+open Errors
 open Util
 open Pp
 open Reduction
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index 84cc8464f..4aad8e738 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.ml4
@@ -25,7 +25,7 @@ let omega_tactic l =
        | "positive" -> Tacinterp.interp <:tactic<zify_positive>>
        | "N" -> Tacinterp.interp <:tactic<zify_N>>
        | "Z" -> Tacinterp.interp <:tactic<zify_op>>
-       | s -> Util.error ("No Omega knowledge base for type "^s))
+       | s -> Errors.error ("No Omega knowledge base for type "^s))
     (Util.list_uniquize (List.sort compare l))
   in
   tclTHEN
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index 1f4ea97fd..4b3385677 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-open Util
+open Pp
 open Tacexpr
 open Quote
 
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index fbb754204..fe025e6da 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -102,6 +102,7 @@
 
 (*i*)
 open Pp
+open Errors
 open Util
 open Names
 open Term
diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml
index 98d6361c0..b3151f26c 100644
--- a/plugins/ring/ring.ml
+++ b/plugins/ring/ring.ml
@@ -9,6 +9,7 @@
 (* ML part of the Ring tactic *)
 
 open Pp
+open Errors
 open Util
 open Flags
 open Term
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index e810e15c1..298b24850 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -39,7 +39,7 @@ let destructurate t =
     | Term.Var id,[] -> Kvar(Names.string_of_id id)
     | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body)
     | Term.Prod (Names.Name _,_,_),[] ->
-	Util.error "Omega: Not a quantifier-free goal"
+	Errors.error "Omega: Not a quantifier-free goal"
     | _ -> Kufo
 
 exception Destruct
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 2db86e005..87e42354b 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -18,7 +18,7 @@ let romega_tactic l =
        | "positive" -> Tacinterp.interp <:tactic<zify_positive>>
        | "N" -> Tacinterp.interp <:tactic<zify_N>>
        | "Z" -> Tacinterp.interp <:tactic<zify_op>>
-       | s -> Util.error ("No ROmega knowledge base for type "^s))
+       | s -> Errors.error ("No ROmega knowledge base for type "^s))
     (Util.list_uniquize (List.sort compare l))
   in
   tclTHEN
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 4a6d462ec..550a4af2b 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -6,6 +6,7 @@
 
  *************************************************************************)
 
+open Errors
 open Util
 open Const_omega
 module OmegaSolver = Omega.MakeOmegaSolver (Bigint)
@@ -450,7 +451,7 @@ let rec scalar n = function
  | Omult(t1,Oint x) ->
      do_list [Lazy.force coq_c_mult_assoc_reduced], Omult(t1,Oint (n*x))
  | Omult(t1,t2) ->
-     Util.error "Omega: Can't solve a goal with non-linear products"
+     Errors.error "Omega: Can't solve a goal with non-linear products"
  | (Oatom _ as t) -> do_list [], Omult(t,Oint n)
  | Oint i -> do_list [Lazy.force coq_c_reduce],Oint(n*i)
  | (Oufo _ as t)-> do_list [], Oufo (Omult(t,Oint n))
@@ -469,7 +470,7 @@ let rec negate = function
  | Omult(t1,Oint x) ->
      do_list [Lazy.force coq_c_opp_mult_r], Omult(t1,Oint (Bigint.neg x))
  | Omult(t1,t2) ->
-     Util.error "Omega: Can't solve a goal with non-linear products"
+     Errors.error "Omega: Can't solve a goal with non-linear products"
  | (Oatom _ as t) ->
      do_list [Lazy.force coq_c_opp_one], Omult(t,Oint(negone))
  | Oint i -> do_list [Lazy.force coq_c_reduce] ,Oint(Bigint.neg i)
@@ -541,7 +542,7 @@ let shrink_pair f1 f2 =
        Lazy.force coq_c_red4, Omult(Oatom v,Oplus(c1,c2))
    | t1,t2 ->
        oprint stdout t1; print_newline (); oprint stdout t2; print_newline ();
-       flush Pervasives.stdout; Util.error "shrink.1"
+       flush Pervasives.stdout; Errors.error "shrink.1"
   end
 
 (* \subsection{Calcul d'une sous formule constante} *)
@@ -555,9 +556,9 @@ let reduce_factor = function
       let rec compute = function
           Oint n -> n
 	| Oplus(t1,t2) -> compute t1 + compute t2
-	| _ -> Util.error "condense.1" in
+	| _ -> Errors.error "condense.1" in
 	[Lazy.force coq_c_reduce], Omult(Oatom v,Oint(compute c))
-  | t -> Util.error "reduce_factor.1"
+  | t -> Errors.error "reduce_factor.1"
 
 (* \subsection{Réordonnancement} *)
 
@@ -1291,7 +1292,7 @@ let total_reflexive_omega_tactic gl =
   let systems_list = destructurate_hyps full_reified_goal in
   if !debug then display_systems systems_list;
   resolution env full_reified_goal systems_list gl
-  with NO_CONTRADICTION -> Util.error "ROmega can't solve this system"
+  with NO_CONTRADICTION -> Errors.error "ROmega can't solve this system"
 
 
 (*i let tester = Tacmach.hide_atomic_tactic "TestOmega" test_tactic i*)
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index d773b1535..2448a2d39 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Term
+open Errors
 open Util
 open Goptions
 
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 4a9a0e47f..60ef81286 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -8,6 +8,7 @@
 
 module Search = Explore.Make(Proof_search)
 
+open Errors
 open Util
 open Term
 open Names
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 9d61c06de..e834650ac 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -9,6 +9,7 @@
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
 open Pp
+open Errors
 open Util
 open Names
 open Term
diff --git a/plugins/subtac/eterm.ml b/plugins/subtac/eterm.ml
index f4d8b769c..0bde8dca9 100644
--- a/plugins/subtac/eterm.ml
+++ b/plugins/subtac/eterm.ml
@@ -11,6 +11,7 @@ open Names
 open Evd
 open List
 open Pp
+open Errors
 open Util
 open Subtac_utils
 open Proof_type
diff --git a/plugins/subtac/eterm.mli b/plugins/subtac/eterm.mli
index 03d76f29a..4812fe0a6 100644
--- a/plugins/subtac/eterm.mli
+++ b/plugins/subtac/eterm.mli
@@ -11,6 +11,7 @@ open Tacmach
 open Term
 open Evd
 open Names
+open Pp
 open Util
 open Tacinterp
 
diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4
index c37f0db5a..27de89f67 100644
--- a/plugins/subtac/g_subtac.ml4
+++ b/plugins/subtac/g_subtac.ml4
@@ -14,7 +14,8 @@
 
 
 open Flags
-open Util
+open Errors
+open Pp
 open Names
 open Nameops
 open Vernacentries
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 710149ae4..cccb12e41 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -9,6 +9,7 @@
 open Compat
 open Global
 open Pp
+open Errors
 open Util
 open Names
 open Sign
diff --git a/plugins/subtac/subtac.mli b/plugins/subtac/subtac.mli
index b51150aa0..32d484091 100644
--- a/plugins/subtac/subtac.mli
+++ b/plugins/subtac/subtac.mli
@@ -1,2 +1,2 @@
 val require_library : string -> unit
-val subtac : Util.loc * Vernacexpr.vernac_expr -> unit
+val subtac : Pp.loc * Vernacexpr.vernac_expr -> unit
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index 16d4e21ee..d60841e72 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Cases
+open Errors
 open Util
 open Names
 open Nameops
diff --git a/plugins/subtac/subtac_cases.mli b/plugins/subtac/subtac_cases.mli
index 77537d33a..11a811597 100644
--- a/plugins/subtac/subtac_cases.mli
+++ b/plugins/subtac/subtac_cases.mli
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 (*i*)
+open Errors
 open Util
 open Names
 open Term
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index cac0988c0..a81243f73 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -22,6 +22,7 @@ open Typeclasses
 open Typeclasses_errors
 open Decl_kinds
 open Entries
+open Errors
 open Util
 
 module SPretyping = Subtac_pretyping.Pretyping
@@ -71,8 +72,8 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
 		let t =
 		  if b then
 		    let _k = class_info cl in
-		      CHole (Util.dummy_loc, Some Evd.InternalHole)
-		  else CHole (Util.dummy_loc, None)
+		      CHole (Pp.dummy_loc, Some Evd.InternalHole)
+		  else CHole (Pp.dummy_loc, None)
 		in t, avoid
 	    | None -> failwith ("new instance: under-applied typeclass"))
 	  cl
@@ -149,7 +150,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
 		      k.cl_projs;
 		    c :: props, rest'
 		with Not_found ->
-		  (CHole (Util.dummy_loc, None) :: props), rest
+		  (CHole (Pp.dummy_loc, None) :: props), rest
 	      else props, rest)
 	    ([], props) k.cl_props
 	in
diff --git a/plugins/subtac/subtac_classes.mli b/plugins/subtac/subtac_classes.mli
index 5b5c02037..5b8636a12 100644
--- a/plugins/subtac/subtac_classes.mli
+++ b/plugins/subtac/subtac_classes.mli
@@ -16,6 +16,7 @@ open Environ
 open Nametab
 open Mod_subst
 open Topconstr
+open Errors
 open Util
 open Typeclasses
 open Implicit_quantifiers
diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml
index eb29bd045..3cbf9fcab 100644
--- a/plugins/subtac/subtac_coercion.ml
+++ b/plugins/subtac/subtac_coercion.ml
@@ -5,6 +5,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
+open Errors
 open Util
 open Names
 open Term
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index ecae6759f..e5d93ace2 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -9,6 +9,7 @@ open Pp
 open Glob_term
 open Sign
 open Tacred
+open Errors
 open Util
 open Names
 open Nameops
diff --git a/plugins/subtac/subtac_errors.ml b/plugins/subtac/subtac_errors.ml
index 067da150e..f07bbeb43 100644
--- a/plugins/subtac/subtac_errors.ml
+++ b/plugins/subtac/subtac_errors.ml
@@ -1,3 +1,4 @@
+open Errors
 open Util
 open Pp
 open Printer
diff --git a/plugins/subtac/subtac_errors.mli b/plugins/subtac/subtac_errors.mli
index 8d75b9c01..c65203075 100644
--- a/plugins/subtac/subtac_errors.mli
+++ b/plugins/subtac/subtac_errors.mli
@@ -1,13 +1,13 @@
 type term_pp = Pp.std_ppcmds
 type subtyping_error =
-    UncoercibleInferType of Util.loc * term_pp * term_pp
-  | UncoercibleInferTerm of Util.loc * term_pp * term_pp * term_pp * term_pp
+    UncoercibleInferType of Pp.loc * term_pp * term_pp
+  | UncoercibleInferTerm of Pp.loc * term_pp * term_pp * term_pp * term_pp
   | UncoercibleRewrite of term_pp * term_pp
 type typing_error =
-    NonFunctionalApp of Util.loc * term_pp * term_pp * term_pp
-  | NonConvertible of Util.loc * term_pp * term_pp
-  | NonSigma of Util.loc * term_pp
-  | IllSorted of Util.loc * term_pp
+    NonFunctionalApp of Pp.loc * term_pp * term_pp * term_pp
+  | NonConvertible of Pp.loc * term_pp * term_pp
+  | NonSigma of Pp.loc * term_pp
+  | IllSorted of Pp.loc * term_pp
 exception Subtyping_error of subtyping_error
 exception Typing_error of typing_error
 exception Debug_msg of string
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 6a5878b3e..527c5e084 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -11,6 +11,7 @@ open Summary
 open Libobject
 open Entries
 open Decl_kinds
+open Errors
 open Util
 open Evd
 open Declare
@@ -18,7 +19,7 @@ open Proof_type
 open Compat
 
 let ppwarn cmd = Pp.warn (str"Program:" ++ cmd)
-let pperror cmd = Util.errorlabstrm "Program" cmd
+let pperror cmd = Errors.errorlabstrm "Program" cmd
 let error s = pperror (str s)
 
 let reduce c =
@@ -551,7 +552,7 @@ and solve_obligation_by_tac prg obls i tac =
 	| Loc.Exc_located(_, Refiner.FailError (_, s))
 	| Refiner.FailError (_, s) ->
 	    user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s)
-	| Util.Anomaly _ as e -> raise e
+	| Errors.Anomaly _ as e -> raise e
 	| e -> false
 
 and solve_prg_obligations prg ?oblset tac =
diff --git a/plugins/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli
index c1d665aac..284e975db 100644
--- a/plugins/subtac/subtac_obligations.mli
+++ b/plugins/subtac/subtac_obligations.mli
@@ -1,4 +1,5 @@
 open Names
+open Pp
 open Util
 open Libnames
 open Evd
diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml
index 7c0d12325..c8acf7e0b 100644
--- a/plugins/subtac/subtac_pretyping.ml
+++ b/plugins/subtac/subtac_pretyping.ml
@@ -8,6 +8,7 @@
 
 open Global
 open Pp
+open Errors
 open Util
 open Names
 open Sign
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 528a2e683..fbeed381d 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -8,6 +8,7 @@
 
 open Pp
 open Compat
+open Errors
 open Util
 open Names
 open Sign
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index 28bbdd35e..0ed78a23b 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -5,6 +5,8 @@ open Libnames
 open Coqlib
 open Term
 open Names
+open Errors
+open Pp
 open Util
 
 let ($) f x = f x
@@ -426,7 +428,7 @@ let pr_meta_map evd =
   in
   prlist pr_meta_binding ml
 
-let pr_idl idl = prlist_with_sep pr_spc pr_id idl
+let pr_idl idl = pr_sequence pr_id idl
 
 let pr_evar_info evi =
   let phyps =
@@ -443,14 +445,14 @@ let pr_evar_info evi =
 
 let pr_evar_map sigma =
   h 0
-    (prlist_with_sep pr_fnl
+    (prlist_with_sep fnl
       (fun (ev,evi) ->
         h 0 (str(string_of_existential ev)++str"=="++ pr_evar_info evi))
       (to_list sigma))
 
 let pr_constraints pbs =
   h 0
-    (prlist_with_sep pr_fnl (fun (pbty,t1,t2) ->
+    (prlist_with_sep fnl (fun (pbty,t1,t2) ->
       Termops.print_constr t1 ++ spc() ++
       str (match pbty with
 	| Reduction.CONV -> "=="
diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli
index de96cc602..70ad0bcc8 100644
--- a/plugins/subtac/subtac_utils.mli
+++ b/plugins/subtac/subtac_utils.mli
@@ -7,6 +7,7 @@ open Evd
 open Decl_kinds
 open Topconstr
 open Glob_term
+open Errors
 open Util
 open Evarutil
 open Names
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index bd2285bb3..cf51af134 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -7,6 +7,7 @@
 (***********************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Pcoq
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index 446ae5225..5a355b971 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -11,6 +11,7 @@
 (*i*)
 open Pcoq
 open Pp
+open Errors
 open Util
 open Names
 open Coqlib
@@ -20,6 +21,7 @@ open Bigint
 open Coqlib
 open Notation
 open Pp
+open Errors
 open Util
 open Names
 (*i*)
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index 19a3c899f..cbc8d7fd6 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -111,7 +111,7 @@ let int31_of_pos_bigint dloc n =
   GApp (dloc, ref_construct, List.rev (args 31 n))
 
 let error_negative dloc =
-  Util.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers.")
+  Errors.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers.")
 
 let interp_int31 dloc n =
   if is_pos_or_zero n then
@@ -143,7 +143,7 @@ let uninterp_int31 i =
 let _ = Notation.declare_numeral_interpreter int31_scope
   (int31_path, int31_module)
   interp_int31
-  ([GRef (Util.dummy_loc, int31_construct)],
+  ([GRef (Pp.dummy_loc, int31_construct)],
    uninterp_int31,
    true)
 
@@ -201,7 +201,7 @@ let bigN_of_pos_bigint dloc n =
   result hght (word_of_pos_bigint dloc hght n)
 
 let bigN_error_negative dloc =
-  Util.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers.")
+  Errors.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers.")
 
 let interp_bigN dloc n =
   if is_pos_or_zero n then
@@ -257,7 +257,7 @@ let uninterp_bigN rc =
 let bigN_list_of_constructors =
   let rec build i =
     if less_than i (add_1 n_inlined) then
-      GRef (Util.dummy_loc, bigN_constructor i)::(build (add_1 i))
+      GRef (Pp.dummy_loc, bigN_constructor i)::(build (add_1 i))
     else
       []
   in
@@ -303,8 +303,8 @@ let uninterp_bigZ rc =
 let _ = Notation.declare_numeral_interpreter bigZ_scope
   (bigZ_path, bigZ_module)
   interp_bigZ
-  ([GRef (Util.dummy_loc, bigZ_pos);
-    GRef (Util.dummy_loc, bigZ_neg)],
+  ([GRef (Pp.dummy_loc, bigZ_pos);
+    GRef (Pp.dummy_loc, bigZ_neg)],
    uninterp_bigZ,
    true)
 
@@ -324,5 +324,5 @@ let uninterp_bigQ rc =
 let _ = Notation.declare_numeral_interpreter bigQ_scope
   (bigQ_path, bigQ_module)
   interp_bigQ
-  ([GRef (Util.dummy_loc, bigQ_z)], uninterp_bigQ,
+  ([GRef (Pp.dummy_loc, bigQ_z)], uninterp_bigQ,
    true)
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index b9c0bcd6f..b3195f281 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Pcoq
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index d670f6026..640806d87 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -7,6 +7,7 @@
 (***********************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Pcoq
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index f8bce8f79..450d57969 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -8,6 +8,7 @@
 
 open Pcoq
 open Pp
+open Errors
 open Util
 open Names
 open Topconstr
diff --git a/plugins/xml/acic2Xml.ml4 b/plugins/xml/acic2Xml.ml4
index 97f7e2bd4..75bc84074 100644
--- a/plugins/xml/acic2Xml.ml4
+++ b/plugins/xml/acic2Xml.ml4
@@ -21,7 +21,7 @@ let typesdtdname = "http://mowgli.cs.unibo.it/dtd/cictypes.dtd";;
 
 let rec find_last_id =
  function
-    [] -> Util.anomaly "find_last_id: empty list"
+    [] -> Errors.anomaly "find_last_id: empty list"
   | [id,_,_] -> id
   | _::tl -> find_last_id tl
 ;;
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index da0a65ff5..78a402898 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
@@ -59,7 +59,7 @@ let get_uri_of_var v pvars =
  let module N = Names in
   let rec search_in_open_sections =
    function
-      [] -> Util.error ("Variable "^v^" not found")
+      [] -> Errors.error ("Variable "^v^" not found")
     | he::tl as modules ->
        let dirpath = N.make_dirpath modules in
         if List.mem (N.id_of_string v) (D.last_section_hyps dirpath) then
@@ -162,7 +162,7 @@ let family_of_term ty =
  match Term.kind_of_term ty with
     Term.Sort s -> Coq_sort (Term.family_of_sort s)
   | Term.Const _ -> CProp  (* I could check that the constant is CProp *)
-  | _ -> Util.anomaly "family_of_term"
+  | _ -> Errors.anomaly "family_of_term"
 ;;
 
 module CPropRetyping =
@@ -177,7 +177,7 @@ module CPropRetyping =
   | h::rest ->
       match T.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma typ) with
         | T.Prod (na,c1,c2) -> subst_type env sigma (T.subst1 h c2) rest
-        | _ -> Util.anomaly "Non-functional construction"
+        | _ -> Errors.anomaly "Non-functional construction"
 
 
   let sort_of_atomic_type env sigma ft args =
@@ -193,7 +193,7 @@ let typeur sigma metamap =
     match Term.kind_of_term cstr with
     | T.Meta n ->
           (try T.strip_outer_cast (List.assoc n metamap)
-           with Not_found -> Util.anomaly "type_of: this is not a well-typed term")
+           with Not_found -> Errors.anomaly "type_of: this is not a well-typed term")
     | T.Rel n ->
         let (_,_,ty) = Environ.lookup_rel n env in
         T.lift n ty
@@ -202,7 +202,7 @@ let typeur sigma metamap =
           let (_,_,ty) = Environ.lookup_named id env in
           ty
         with Not_found ->
-          Util.anomaly ("type_of: variable "^(Names.string_of_id id)^" unbound"))
+          Errors.anomaly ("type_of: variable "^(Names.string_of_id id)^" unbound"))
     | T.Const c ->
         let cb = Environ.lookup_constant c env in
         Typeops.type_of_constant_type env (cb.Declarations.const_type)
@@ -212,7 +212,7 @@ let typeur sigma metamap =
     | T.Case (_,p,c,lf) ->
         let Inductiveops.IndType(_,realargs) =
           try Inductiveops.find_rectype env sigma (type_of env c)
-          with Not_found -> Util.anomaly "type_of: Bad recursive type" in
+          with Not_found -> Errors.anomaly "type_of: Bad recursive type" in
         let t = Reductionops.whd_beta sigma (T.applist (p, realargs)) in
         (match Term.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma (type_of env t)) with
           | T.Prod _ -> Reductionops.whd_beta sigma (T.applist (t, [c]))
@@ -253,7 +253,7 @@ let typeur sigma metamap =
           | _, (CProp as s) -> s)
     | T.App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args
     | T.Lambda _ | T.Fix _ | T.Construct _ ->
-        Util.anomaly "sort_of: Not a type (1)"
+        Errors.anomaly "sort_of: Not a type (1)"
     | _ -> outsort env sigma (type_of env t)
 
   and sort_family_of env t =
@@ -265,7 +265,7 @@ let typeur sigma metamap =
     | T.App(f,args) ->
        sort_of_atomic_type env sigma (type_of env f) args
     | T.Lambda _ | T.Fix _ | T.Construct _ ->
-        Util.anomaly "sort_of: Not a type (1)"
+        Errors.anomaly "sort_of: Not a type (1)"
     | _ -> outsort env sigma (type_of env t)
 
   in type_of, sort_of, sort_family_of
@@ -523,7 +523,7 @@ print_endline "PASSATO" ; flush stdout ;
                add_inner_type fresh_id'' ;
               A.AEvar
                (fresh_id'', n, Array.to_list (Array.map (aux' env idrefs) l))
-           | T.Meta _ -> Util.anomaly "Meta met during exporting to XML"
+           | T.Meta _ -> Errors.anomaly "Meta met during exporting to XML"
            | T.Sort s -> A.ASort (fresh_id'', s)
            | T.Cast (v,_, t) ->
               Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
@@ -737,7 +737,7 @@ print_endline "PASSATO" ; flush stdout ;
                 let ids = ref (Termops.ids_of_context env) in
                  Array.map
                   (function
-                      N.Anonymous -> Util.error "Anonymous fix function met"
+                      N.Anonymous -> Errors.error "Anonymous fix function met"
                     | N.Name id as n ->
                        let res = N.Name (Namegen.next_name_away n !ids) in
                         ids := id::!ids ;
@@ -750,7 +750,7 @@ print_endline "PASSATO" ; flush stdout ;
                     let fi' =
                      match fi with
                         N.Name fi -> fi
-                      | N.Anonymous -> Util.error "Anonymous fix function met"
+                      | N.Anonymous -> Errors.error "Anonymous fix function met"
                     in
                      (id, fi', ai,
                       aux' env idrefs ti,
@@ -771,7 +771,7 @@ print_endline "PASSATO" ; flush stdout ;
                 let ids = ref (Termops.ids_of_context env) in
                  Array.map
                   (function
-                      N.Anonymous -> Util.error "Anonymous fix function met"
+                      N.Anonymous -> Errors.error "Anonymous fix function met"
                     | N.Name id as n ->
                        let res = N.Name (Namegen.next_name_away n !ids) in
                         ids := id::!ids ;
@@ -784,7 +784,7 @@ print_endline "PASSATO" ; flush stdout ;
                     let fi' =
                      match fi with
                         N.Name fi -> fi
-                      | N.Anonymous -> Util.error "Anonymous fix function met"
+                      | N.Anonymous -> Errors.error "Anonymous fix function met"
                     in
                      (id, fi',
                       aux' env idrefs ti,
diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml
index a21a919ad..30cd5c18b 100644
--- a/plugins/xml/doubleTypeInference.ml
+++ b/plugins/xml/doubleTypeInference.ml
@@ -67,7 +67,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
    let judgement =
     match T.kind_of_term cstr with
        T.Meta n ->
-        Util.error
+        Errors.error
          "DoubleTypeInference.double_type_of: found a non-instanciated goal"
 
      | T.Evar ((n,l) as ev) ->
diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4
index 3c3e54fa3..69b9e6ea7 100644
--- a/plugins/xml/dumptree.ml4
+++ b/plugins/xml/dumptree.ml4
@@ -128,7 +128,7 @@ let pr_goal_xml sigma g =
 ;;
 
 let print_proof_xml () =
-  Util.anomaly "Dump Tree command not supported in this version."
+  Errors.anomaly "Dump Tree command not supported in this version."
 
 
 VERNAC COMMAND EXTEND DumpTree
diff --git a/plugins/xml/proofTree2Xml.ml4 b/plugins/xml/proofTree2Xml.ml4
index 2f5eb6ac2..21058a7b9 100644
--- a/plugins/xml/proofTree2Xml.ml4
+++ b/plugins/xml/proofTree2Xml.ml4
@@ -53,7 +53,7 @@ let constr_to_xml obj sigma env =
     in
      Acic2Xml.print_term ids_to_inner_sorts annobj
    with e ->
-    Util.anomaly
+    Errors.anomaly
      ("Problem during the conversion of constr into XML: " ^
       Printexc.to_string e)
 (* CSC: debugging stuff
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 1037bbf08..13821488a 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -424,7 +424,7 @@ let kind_of_variable id =
     | DK.IsAssumption DK.Conjectural -> "VARIABLE","Conjecture"
     | DK.IsDefinition DK.Definition -> "VARIABLE","LocalDefinition"
     | DK.IsProof _ -> "VARIABLE","LocalFact"
-    | _ -> Util.anomaly "Unsupported variable kind"
+    | _ -> Errors.anomaly "Unsupported variable kind"
 ;;
 
 let kind_of_constant kn =
@@ -541,7 +541,7 @@ let print internal glob_ref kind xml_library_root =
             D.mind_finite=finite} = mib in
           Cic2acic.Inductive kn,mk_inductive_obj kn mib packs variables nparams hyps finite
     | Ln.ConstructRef _ ->
-       Util.error ("a single constructor cannot be printed in XML")
+       Errors.error ("a single constructor cannot be printed in XML")
   in
   let fn = filename_of_path xml_library_root tag in
   let uri = Cic2acic.uri_of_kernel_name tag in
@@ -560,7 +560,7 @@ let print_ref qid fn =
 (* pretty prints via Xml.pp the proof in progress on dest     *)
 let show_pftreestate internal fn (kind,pftst) id =
  if true then
-   Util.anomaly "Xmlcommand.show_pftreestate is not supported in this version."
+   Errors.anomaly "Xmlcommand.show_pftreestate is not supported in this version."
 
 let show fn =
  let pftst = Pfedit.get_pftreestate () in
@@ -656,7 +656,7 @@ let _ =
 	  let options = " --html -s --body-only --no-index --latin1 --raw-comments" in
           let command cmd =
            if Sys.command cmd <> 0 then
-            Util.anomaly ("Error executing \"" ^ cmd ^ "\"")
+            Errors.anomaly ("Error executing \"" ^ cmd ^ "\"")
           in
            command (coqdoc^options^" -o "^fn^".xml "^fn^".v");
            command ("rm "^fn^".v "^fn^".glob");