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

20 files changed, 149 insertions, 136 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index d06c6f2e6b..9d2c1c7ab0 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Nameops
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index abd67236ac..04f5326543 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Names
 open Term
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index eb935d05de..45765805fa 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Nameops
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 49a961f5d2..a14f261e90 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Names
 open Term
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 36268de1ee..c606600d76 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Names
 open Term
diff --git a/proofs/goal.ml b/proofs/goal.ml
index d68ab8c55c..f0ab31c5b8 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -10,7 +10,7 @@ open Pp
 open Term
 
 (* This module implements the abstract interface to goals *)
-(* A general invariant of the module, is that a goal whose associated 
+(* A general invariant of the module, is that a goal whose associated
    evar is defined in the current evar_map, should not be accessed. *)
 
 (* type of the goals *)
@@ -47,22 +47,22 @@ let get_by_uid u =
      for instance. *)
   build (int_of_string u)
 
-(* Builds a new goal with content evar [e] and 
+(* Builds a new goal with content evar [e] and
    inheriting from goal [gl]*)
 let descendent gl e =
   { gl with content = e}
 
-(* [advance sigma g] returns [Some g'] if [g'] is undefined and 
+(* [advance sigma g] returns [Some g'] if [g'] is undefined and
     is the current avatar of [g] (for instance [g] was changed by [clear]
     into [g']). It returns [None] if [g] has been (partially) solved. *)
 open Store.Field
 let rec advance sigma g =
   let evi = Evd.find sigma g.content in
   if Option.default false (Evarutil.cleared.get evi.Evd.evar_extra) then
-    let v = 
-      match evi.Evd.evar_body with 
+    let v =
+      match evi.Evd.evar_body with
       | Evd.Evar_defined c -> c
-      | _ -> Util.anomaly "Some goal is marked as 'cleared' but is uninstantiated"
+      | _ -> Errors.anomaly "Some goal is marked as 'cleared' but is uninstantiated"
     in
     let (e,_) = Term.destEvar v in
     let g' = { g with content = e } in
@@ -81,10 +81,10 @@ type subgoals = { subgoals: goal list }
 (* type of the base elements of the goal API.*)
 (* it has an extra evar_info with respect to what would be expected,
    it is supposed to be the evar_info of the goal in the evar_map.
-   The idea is that it is computed by the [run] function as an 
-   optimisation, since it will generaly not change during the 
+   The idea is that it is computed by the [run] function as an
+   optimisation, since it will generaly not change during the
    evaluation. *)
-type 'a sensitive = 
+type 'a sensitive =
     Environ.env -> Evd.evar_map ref -> goal -> Evd.evar_info -> 'a
 
 (* evaluates a goal sensitive value in a given goal (knowing the current evar_map). *)
@@ -105,7 +105,7 @@ let bind e f env rdefs goal info =
 let return v _ _ _ _ = v
 
 (* interpretation of "open" constr *)
-(* spiwack: it is a wrapper around [Constrintern.interp_open_constr]. 
+(* spiwack: it is a wrapper around [Constrintern.interp_open_constr].
     In an ideal world, this could/should be the other way round.
     As of now, though, it seems at least quite useful to build tactics. *)
 let interp_constr cexpr env rdefs _ _ =
@@ -114,7 +114,7 @@ let interp_constr cexpr env rdefs _ _ =
   c
 
 (* Type of constr with holes used by refine. *)
-(* The list of evars doesn't necessarily contain all the evars in the constr, 
+(* The list of evars doesn't necessarily contain all the evars in the constr,
     only those the constr has introduced. *)
 (* The variables in [myevars] are supposed to be stored
    in decreasing order. Breaking this invariant might cause
@@ -129,7 +129,7 @@ module Refinable = struct
 
   type handle = Evd.evar list ref
 
-  let make t env rdefs gl info = 
+  let make t env rdefs gl info =
     let r = ref [] in
     let me = t r env rdefs gl info in
     { me = me;
@@ -144,9 +144,9 @@ module Refinable = struct
     let (e,_) = Term.destEvar ev in
     handle := e::!handle;
     ev
-      
+
   (* [with_type c typ] constrains term [c] to have type [typ].  *)
-  let with_type t typ env rdefs _ _ = 
+  let with_type t typ env rdefs _ _ =
     (* spiwack: this function assumes that no evars can be created during
         this sort of coercion.
         If it is not the case it could produce bugs. We would need to add a handle
@@ -154,13 +154,13 @@ module Refinable = struct
     let my_type = Retyping.get_type_of env !rdefs t in
     let j = Environ.make_judge t my_type in
     let tycon = Evarutil.mk_tycon_type typ in
-    let (new_defs,j') = 
-      Coercion.Default.inh_conv_coerce_to (Util.dummy_loc) env !rdefs j tycon 
+    let (new_defs,j') =
+      Coercion.Default.inh_conv_coerce_to (Pp.dummy_loc) env !rdefs j tycon
     in
     rdefs := new_defs;
-    j'.Environ.uj_val 
+    j'.Environ.uj_val
 
-  (* spiwack: it is not very fine grain since it solves all typeclasses holes, 
+  (* spiwack: it is not very fine grain since it solves all typeclasses holes,
       not only those containing the current goal, or a given term. But it
       seems to fit our needs so far. *)
   let resolve_typeclasses ?onlyargs ?split ?(fail=false) () env rdefs _ _ =
@@ -214,23 +214,23 @@ module Refinable = struct
   let constr_of_raw handle check_type resolve_classes rawc env rdefs gl info =
     (* We need to keep trace of what [rdefs] was originally*)
     let init_defs = !rdefs in
-    (* if [check_type] is true, then creates a type constraint for the 
+    (* if [check_type] is true, then creates a type constraint for the
        proof-to-be *)
     let tycon = Pretyping.OfType (Option.init check_type (Evd.evar_concl info)) in
     (* call to [understand_tcc_evars] returns a constr with undefined evars
        these evars will be our new goals *)
-    let open_constr = 
+    let open_constr =
       Pretyping.Default.understand_tcc_evars ~resolve_classes rdefs env tycon rawc
     in
       ignore(update_handle handle init_defs !rdefs);
-      open_constr 
-  
+      open_constr
+
   let constr_of_open_constr handle check_type (evars, c) env rdefs gl info =
     let delta = update_handle handle !rdefs evars in
       rdefs := Evd.fold (fun ev evi evd -> Evd.add evd ev evi) delta !rdefs;
       if check_type then with_type c (Evd.evar_concl (content !rdefs gl)) env rdefs gl info
       else c
- 
+
 end
 
 (* [refine t] takes a refinable term and use it as a partial proof for current
@@ -245,10 +245,10 @@ let refine step env rdefs gl info =
   (* creates the new [evar_map] by defining the evar of the current goal
      as being [refine_step]. *)
   let new_defs = Evd.define gl.content (step.me) !rdefs in
-  rdefs := new_defs;   
+  rdefs := new_defs;
   (* Filtering the [subgoals] for uninstanciated (=unsolved) goals. *)
-  let subgoals = 
-    Option.List.flatten (List.map (advance !rdefs) subgoals) 
+  let subgoals =
+    Option.List.flatten (List.map (advance !rdefs) subgoals)
   in
   { subgoals = subgoals }
 
@@ -267,12 +267,12 @@ let clear ids env rdefs gl info =
   { subgoals = [cleared_goal] }
 
 let wrap_apply_to_hyp_and_dependent_on sign id f g =
-  try Environ.apply_to_hyp_and_dependent_on sign id f g 
-  with Environ.Hyp_not_found -> 
-    Util.error "No such assumption" 
+  try Environ.apply_to_hyp_and_dependent_on sign id f g
+  with Environ.Hyp_not_found ->
+    Errors.error "No such assumption"
 
 let check_typability env sigma c =
-  let _ = Typing.type_of env sigma c in () 
+  let _ = Typing.type_of env sigma c in ()
 
 let recheck_typability (what,id) env sigma t =
   try check_typability env sigma t
@@ -280,7 +280,7 @@ let recheck_typability (what,id) env sigma t =
     let s = match what with
       | None -> "the conclusion"
       | Some id -> "hypothesis "^(Names.string_of_id id) in
-    Util.error
+    Errors.error
       ("The correctness of "^s^" relies on the body of "^(Names.string_of_id id))
 
 let remove_hyp_body env sigma id =
@@ -288,11 +288,11 @@ let remove_hyp_body env sigma id =
     wrap_apply_to_hyp_and_dependent_on (Environ.named_context_val env) id
       (fun (_,c,t) _ ->
 	match c with
-	| None -> Util.error ((Names.string_of_id id)^" is not a local definition")
+	| None -> Errors.error ((Names.string_of_id id)^" is not a local definition")
 	| Some c ->(id,None,t))
       (fun (id',c,t as d) sign ->
 	(
-	  begin 
+	  begin
 	    let env = Environ.reset_with_named_context sign env in
 	    match c with
 	    | None ->  recheck_typability (Some id',id) env sigma t
@@ -301,18 +301,18 @@ let remove_hyp_body env sigma id =
 		recheck_typability (Some id',id) env sigma b'
 	  end;d))
   in
-  Environ.reset_with_named_context sign env 
+  Environ.reset_with_named_context sign env
 
 
 let clear_body idents env rdefs gl info =
   let info = content !rdefs gl in
   let full_env = Environ.reset_with_named_context (Evd.evar_hyps info) env in
-  let aux env id = 
+  let aux env id =
      let env' = remove_hyp_body env !rdefs id in
        recheck_typability (None,id) env' !rdefs (Evd.evar_concl info);
        env'
   in
-  let new_env = 
+  let new_env =
     List.fold_left aux full_env idents
   in
   let concl = Evd.evar_concl info in
@@ -334,7 +334,7 @@ let concl _ _ _ info =
 let hyps _ _ _ info =
   Evd.evar_hyps info
 
-(* [env] is the current [Environ.env] containing both the 
+(* [env] is the current [Environ.env] containing both the
    environment in which the proof is ran, and the goal hypotheses *)
 let env env _ _ _ = env
 
@@ -359,7 +359,7 @@ let equal { content = e1 } { content = e2 } = e1 = e2
 let here goal value _ _ goal' _ =
   if equal goal goal' then
     value
-  else 
+  else
     raise UndefinedHere
 
 (* arnaud: voir à la passer dans Util ? *)
@@ -384,52 +384,52 @@ let convert_hyp check (id,b,bt as d) env rdefs gl info =
   let replace_function =
     (fun _ (_,c,ct) _ ->
        if check && not (Reductionops.is_conv env sigma bt ct) then
-	 Util.error ("Incorrect change of the type of "^(Names.string_of_id id));
+	 Errors.error ("Incorrect change of the type of "^(Names.string_of_id id));
        if check && not (Option.Misc.compare (Reductionops.is_conv env sigma) b c) then
-	 Util.error ("Incorrect change of the body of "^(Names.string_of_id id));
+	 Errors.error ("Incorrect change of the body of "^(Names.string_of_id id));
        d)
   in
   (* Modified named context. *)
-  let new_hyps = 
+  let new_hyps =
     Environ.apply_to_hyp (hyps env rdefs gl info) id replace_function
-  in  
+  in
   let new_env = Environ.reset_with_named_context new_hyps env in
-  let new_constr = 
+  let new_constr =
     Evarutil.e_new_evar rdefs new_env (concl env rdefs gl info)
   in
   let (new_evar,_) = Term.destEvar new_constr in
   let new_goal = descendent gl new_evar in
   rdefs := Evd.define gl.content new_constr !rdefs;
   { subgoals = [new_goal] }
-  
+
 let convert_concl check cl' env rdefs gl info =
   let sigma = !rdefs in
   let cl = concl env rdefs gl info in
   check_typability env sigma cl';
   if (not check) || Reductionops.is_conv_leq env sigma cl' cl then
-    let new_constr = 
-      Evarutil.e_new_evar rdefs env cl' 
+    let new_constr =
+      Evarutil.e_new_evar rdefs env cl'
     in
     let (new_evar,_) = Term.destEvar new_constr in
     let new_goal = descendent gl new_evar in
     rdefs := Evd.define gl.content new_constr !rdefs;
     { subgoals = [new_goal] }
   else
-    Util.error "convert-concl rule passed non-converting term"
+    Errors.error "convert-concl rule passed non-converting term"
 
 
-(*** Bureaucracy in hypotheses ***)  
+(*** Bureaucracy in hypotheses ***)
 
 (* Renames a hypothesis. *)
 let rename_hyp_sign id1 id2 sign =
   Environ.apply_to_hyp_and_dependent_on sign id1
     (fun (_,b,t) _ -> (id2,b,t))
     (fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d)
-let rename_hyp id1 id2 env rdefs gl info = 
+let rename_hyp id1 id2 env rdefs gl info =
   let hyps = hyps env rdefs gl info in
   if id1 <> id2 &&
     List.mem id2 (Termops.ids_of_named_context (Environ.named_context_of_val hyps)) then
-       Util.error ((Names.string_of_id id2)^" is already used.");
+       Errors.error ((Names.string_of_id id2)^" is already used.");
   let new_hyps = rename_hyp_sign id1 id2 hyps in
   let new_env = Environ.reset_with_named_context new_hyps env in
   let new_concl = Term.replace_vars [id1,mkVar id2] (concl env rdefs gl info) in
@@ -442,13 +442,13 @@ let rename_hyp id1 id2 env rdefs gl info =
 
 (*** Additional functions ***)
 
-(* emulates List.map for functions of type 
+(* emulates List.map for functions of type
    [Evd.evar_map -> 'a -> 'b * Evd.evar_map] on lists of type 'a, by propagating
    new evar_map to next definition. *)
 (*This sort of construction actually works with any monad (here the State monade
    in Haskell). There is a generic construction in Haskell called mapM.
 *)
-let rec list_map f l s = 
+let rec list_map f l s =
   match l with
   | [] -> ([],s)
   | a::l -> let (a,s) = f s a in
@@ -456,18 +456,18 @@ let rec list_map f l s =
 	       (a::l,s)
 
 
-(* Layer to implement v8.2 tactic engine ontop of the new architecture. 
+(* Layer to implement v8.2 tactic engine ontop of the new architecture.
    Types are different from what they used to be due to a change of the
    internal types. *)
 module V82 = struct
 
   (* Old style env primitive *)
-  let env evars gl = 
+  let env evars gl =
     let evi = content evars gl in
     Evd.evar_env evi
 
   (* For printing *)
-  let unfiltered_env evars gl = 
+  let unfiltered_env evars gl =
     let evi = content evars gl in
     Evd.evar_unfiltered_env evi
 
@@ -494,14 +494,14 @@ module V82 = struct
   (* Old style mk_goal primitive *)
   let mk_goal evars hyps concl extra =
     let evk = Evarutil.new_untyped_evar () in
-    let evi = { Evd.evar_hyps = hyps; 
-		     Evd.evar_concl = concl; 
-		     Evd.evar_filter = List.map (fun _ -> true) 
-	                                                        (Environ.named_context_of_val hyps);
-		     Evd.evar_body = Evd.Evar_empty; 
-		     Evd.evar_source = (Util.dummy_loc,Evd.GoalEvar);
-		     Evd.evar_candidates = None;
-		     Evd.evar_extra = extra }
+    let evi = { Evd.evar_hyps = hyps;
+		Evd.evar_concl = concl;
+		Evd.evar_filter = List.map (fun _ -> true)
+	(Environ.named_context_of_val hyps);
+		Evd.evar_body = Evd.Evar_empty;
+		Evd.evar_source = (Pp.dummy_loc,Evd.GoalEvar);
+		Evd.evar_candidates = None;
+		Evd.evar_extra = extra }
     in
     let evi = Typeclasses.mark_unresolvable evi in
     let evars = Evd.add evars evk evi in
@@ -518,7 +518,7 @@ module V82 = struct
 
   (* Creates a dummy [goal sigma] for use in auto *)
   let dummy_goal =
-    (* This goal seems to be marshalled somewhere. Therefore it cannot be 
+    (* This goal seems to be marshalled somewhere. Therefore it cannot be
        marked unresolvable for typeclasses, as non-empty Store.t-s happen
        to have functional content. *)
     let evi = Evd.make_evar Environ.empty_named_context_val Term.mkProp in
@@ -532,14 +532,14 @@ module V82 = struct
   (* Instantiates a goal with an open term *)
   let partial_solution sigma { content=evk } c =
     Evd.define evk c sigma
-   
+
   (* Parts of the progress tactical *)
   let same_goal evars1 gl1 evars2 gl2 =
     let evi1 = content evars1 gl1 in
     let evi2 = content evars2 gl2 in
     Term.eq_constr evi1.Evd.evar_concl evi2.Evd.evar_concl &&
     Environ.eq_named_context_val evi1.Evd.evar_hyps evi2.Evd.evar_hyps
-      
+
   let weak_progress glss gls =
     match glss.Evd.it with
     | [ g ] -> not (same_goal glss.Evd.sigma g gls.Evd.sigma gls.Evd.it)
@@ -548,12 +548,12 @@ module V82 = struct
   let progress glss gls =
     weak_progress glss gls
     (* spiwack: progress normally goes like this:
-    (Evd.progress_evar_map gls.Evd.sigma glss.Evd.sigma) || (weak_progress glss gls) 
+    (Evd.progress_evar_map gls.Evd.sigma glss.Evd.sigma) || (weak_progress glss gls)
        This is immensly slow in the current implementation. Maybe we could
        reimplement progress_evar_map with restricted folds like "fold_undefined",
        with a good implementation of them.
     *)
-      
+
   (* Used for congruence closure *)
   let new_goal_with sigma gl new_hyps =
     let evi = content sigma gl in
@@ -571,12 +571,12 @@ module V82 = struct
     (gl,sigma)
 
   (* Goal represented as a type, doesn't take into account section variables *)
-  let abstract_type sigma gl = 
+  let abstract_type sigma gl =
     let (gl,sigma) = nf_evar sigma gl in
     let env = env sigma gl in
     let genv = Global.env () in
-    let is_proof_var decl = 
-      try ignore (Environ.lookup_named (Util.pi1 decl) genv); false 
+    let is_proof_var decl =
+      try ignore (Environ.lookup_named (Util.pi1 decl) genv); false
       with Not_found -> true in
     Environ.fold_named_context_reverse (fun t decl ->
 					  if is_proof_var decl then
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 5babd03a86..c7df86e1f7 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -8,6 +8,7 @@
 
 open Compat
 open Pp
+open Errors
 open Util
 open Names
 open Nameops
@@ -48,7 +49,7 @@ open Pretype_errors
 let rec catchable_exception = function
   | Loc.Exc_located(_,e) -> catchable_exception e
   | LtacLocated(_,e) -> catchable_exception e
-  | Util.UserError _ | TypeError _ | PretypeError (_,_,TypingError _)
+  | Errors.UserError _ | TypeError _ | PretypeError (_,_,TypingError _)
   | RefinerError _ | Indrec.RecursionSchemeError _
   | Nametab.GlobalizationError _ | PretypeError (_,_,VarNotFound _)
   (* reduction errors *)
@@ -179,7 +180,7 @@ let reorder_context env sign ord =
             errorlabstrm "reorder_context"
               (str "Cannot move declaration " ++ pr_id top ++ spc() ++
               str "before " ++
-              prlist_with_sep pr_spc pr_id
+              pr_sequence pr_id
                 (Idset.elements (Idset.inter h
                   (global_vars_set_of_decl env d))));
           step ord' expected ctxt_head mh (d::ctxt_tail)
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 3d507f3583..9be475ac42 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Nameops
@@ -79,7 +80,7 @@ let cook_proof hook =
   hook prf;
   match Proof_global.close_proof () with
   | (i,([e],cg,str,h)) -> (i,(e,cg,str,h))
-  | _ -> Util.anomaly "Pfedit.cook_proof: more than one proof term."
+  | _ -> Errors.anomaly "Pfedit.cook_proof: more than one proof term."
 
 let xml_cook_proof = ref (fun _ -> ())
 let set_xml_cook_proof f = xml_cook_proof := f
@@ -98,7 +99,7 @@ let get_used_variables () =
 
 exception NoSuchGoal
 let _ = Errors.register_handler begin function
-  | NoSuchGoal -> Util.error "No such goal."
+  | NoSuchGoal -> Errors.error "No such goal."
   | _ -> raise Errors.Unhandled
 end
 let get_nth_V82_goal i =
@@ -112,11 +113,11 @@ let get_goal_context_gen i =
   try
     let { it=goal ; sigma=sigma } =  get_nth_V82_goal i in
     (sigma, Refiner.pf_env { it=goal ; sigma=sigma })
-  with Proof_global.NoCurrentProof -> Util.error "No focused proof."
+  with Proof_global.NoCurrentProof -> Errors.error "No focused proof."
 
 let get_goal_context i =
   try get_goal_context_gen i
-  with NoSuchGoal -> Util.error "No such goal."
+  with NoSuchGoal -> Errors.error "No such goal."
 
 let get_current_goal_context () =
   try get_goal_context_gen 1
@@ -128,7 +129,7 @@ let get_current_goal_context () =
 let current_proof_statement () =
   match Proof_global.V82.get_current_initial_conclusions () with
     | (id,([concl],strength,hook)) -> id,strength,concl,hook
-    | _ -> Util.anomaly "Pfedit.current_proof_statement: more than one statement"
+    | _ -> Errors.anomaly "Pfedit.current_proof_statement: more than one statement"
 
 let solve_nth ?(with_end_tac=false) gi tac = 
   try 
@@ -140,10 +141,10 @@ let solve_nth ?(with_end_tac=false) gi tac =
     in
     Proof_global.run_tactic (Proofview.tclFOCUS gi gi tac) 
   with 
-    | Proof_global.NoCurrentProof  -> Util.error "No focused proof"
+    | Proof_global.NoCurrentProof  -> Errors.error "No focused proof"
     | Proofview.IndexOutOfRange | Failure "list_chop" -> 
 	let msg = str "No such goal: " ++ int gi ++ str "." in
-	Util.errorlabstrm "" msg
+	Errors.errorlabstrm "" msg
 
 let by = solve_nth 1
 
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 7297b975f8..e8b0042008 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Pp
 open Names
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 871e68acfc..42a522b7c8 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -102,7 +102,7 @@ end
 exception CannotUnfocusThisWay
 let _ = Errors.register_handler begin function
   | CannotUnfocusThisWay ->
-    Util.error "This proof is focused, but cannot be unfocused this way"
+    Errors.error "This proof is focused, but cannot be unfocused this way"
   | _ -> raise Errors.Unhandled
 end
 
@@ -184,7 +184,7 @@ let push_focus cond inf context pr =
 
 exception FullyUnfocused
 let _ = Errors.register_handler begin function
-  | FullyUnfocused -> Util.error "The proof is not focused"
+  | FullyUnfocused -> Errors.error "The proof is not focused"
   | _ -> raise Errors.Unhandled
 end
 (* An auxiliary function to read the kind of the next focusing step *)
@@ -211,7 +211,7 @@ let push_undo save pr =
 (* Auxiliary function to pop and read a [save_state] from the undo stack. *)
 exception EmptyUndoStack
 let _ = Errors.register_handler begin function
-  | EmptyUndoStack -> Util.error "Cannot undo: no more undo information"
+  | EmptyUndoStack -> Errors.error "Cannot undo: no more undo information"
   | _ -> raise Errors.Unhandled
 end
 let pop_undo pr =
@@ -387,8 +387,8 @@ let start goals =
 exception UnfinishedProof
 exception HasUnresolvedEvar
 let _ = Errors.register_handler begin function
-  | UnfinishedProof -> Util.error "Some goals have not been solved."
-  | HasUnresolvedEvar -> Util.error "Some existential variables are uninstantiated."
+  | UnfinishedProof -> Errors.error "Some goals have not been solved."
+  | HasUnresolvedEvar -> Errors.error "Some existential variables are uninstantiated."
   | _ -> raise Errors.Unhandled
 end
 let return p =
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 9d5ba230e5..63bc4a7080 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -32,7 +32,7 @@ let proof_modes = Hashtbl.create 6
 let find_proof_mode n =
   try Hashtbl.find proof_modes n
   with Not_found ->
-    Util.error (Format.sprintf "No proof mode named \"%s\"." n)
+    Errors.error (Format.sprintf "No proof mode named \"%s\"." n)
 
 let register_proof_mode ({ name = n } as m) = Hashtbl.add proof_modes n m
 (* initial mode: standard mode *)
@@ -48,10 +48,10 @@ let _ =
     optdepr = false;
     optname = "default proof mode" ;
     optkey = ["Default";"Proof";"Mode"] ;
-    optread = begin fun () -> 
-                               let { name = name } = !default_proof_mode in name 
+    optread = begin fun () ->
+                               let { name = name } = !default_proof_mode in name
                      end;
-    optwrite = begin fun n -> 
+    optwrite = begin fun n ->
                                 default_proof_mode := find_proof_mode n
                       end
   }
@@ -63,14 +63,14 @@ type nproof = identifier*Proof.proof
 
 (* Extra info on proofs. *)
 type lemma_possible_guards = int list list
-type proof_info = { 
+type proof_info = {
   strength : Decl_kinds.goal_kind ;
-  compute_guard :  lemma_possible_guards; 
+  compute_guard :  lemma_possible_guards;
   hook :Tacexpr.declaration_hook ;
   mode : proof_mode
 }
 
-(* Invariant: a proof is at most in one of current_proof and suspended. And the 
+(* Invariant: a proof is at most in one of current_proof and suspended. And the
    domain of proof_info is the union of that of current_proof and suspended.*)
 (* The head of [!current_proof] is the actual current proof, the other ones are to
     be resumed when the current proof is closed, aborted or suspended. *)
@@ -82,15 +82,15 @@ let proof_info = ref (Idmap.empty : proof_info Idmap.t)
 let current_proof_mode = ref !default_proof_mode
 
 (* combinators for proof modes *)
-let update_proof_mode () = 
+let update_proof_mode () =
   match !current_proof with
-  | (id,_)::_ ->  
+  | (id,_)::_ ->
       let { mode = m } = Idmap.find id !proof_info in
       !current_proof_mode.reset ();
       current_proof_mode := m;
       !current_proof_mode.set ()
-  | _ -> 
-      !current_proof_mode.reset (); 
+  | _ ->
+      !current_proof_mode.reset ();
       current_proof_mode := standard
 
 (* combinators for the current_proof and suspended lists *)
@@ -99,10 +99,10 @@ let push a l = l := a::!l;
 
 exception NoSuchProof
 let _ = Errors.register_handler begin function
-  | NoSuchProof -> Util.error "No such proof."
+  | NoSuchProof -> Errors.error "No such proof."
   | _ -> raise Errors.Unhandled
 end
-let rec extract id l = 
+let rec extract id l =
   let rec aux = function
     | ((id',_) as np)::l when id_ord id id' = 0 -> (np,l)
     | np::l -> let (np', l) = aux l in (np' , np::l)
@@ -115,13 +115,13 @@ let rec extract id l =
 
 exception NoCurrentProof
 let _ = Errors.register_handler begin function
-  | NoCurrentProof -> Util.error "No focused proof (No proof-editing in progress)."
+  | NoCurrentProof -> Errors.error "No focused proof (No proof-editing in progress)."
   | _ -> raise Errors.Unhandled
 end
 let extract_top l =
   match !l with
   | np::l' -> l := l' ; update_proof_mode (); np
-  | [] -> raise NoCurrentProof	
+  | [] -> raise NoCurrentProof
 let find_top l =
   match !l with
   | np::_ -> np
@@ -134,7 +134,7 @@ let rotate_top l1 l2 =
 let rotate_find id l1 l2 =
   let np = extract id l1 in
   push np l2
-  
+
 
 (* combinators for the proof_info map *)
 let add id info m =
@@ -148,7 +148,7 @@ let get_all_proof_names () =
     List.map fst !current_proof @
     List.map fst !suspended
 
-let give_me_the_proof () = 
+let give_me_the_proof () =
   snd (find_top current_proof)
 
 let get_current_proof_name () =
@@ -157,14 +157,14 @@ let get_current_proof_name () =
 (* spiwack: it might be considered to move error messages away.
     Or else to remove special exceptions from Proof_global.
     Arguments for the former: there is no reason Proof_global is only
-    accessed directly through vernacular commands. Error message should be 
+    accessed directly through vernacular commands. Error message should be
    pushed to external layers, and so we should be able to have a finer
    control on error message on complex actions. *)
 let msg_proofs use_resume =
   match get_all_proof_names () with
     | [] -> (spc () ++ str"(No proof-editing in progress).")
     | l ->  (str"." ++ fnl () ++ str"Proofs currently edited:" ++ spc () ++
-               (Util.prlist_with_sep Util.pr_spc Nameops.pr_id l) ++
+               (pr_sequence Nameops.pr_id l) ++
 	       str"." ++
                (if use_resume then (fnl () ++ str"Use \"Resume\" first.")
               	else (mt ()))
@@ -173,14 +173,14 @@ let msg_proofs use_resume =
 
 let there_is_a_proof () = !current_proof <> []
 let there_are_suspended_proofs () = !suspended <> []
-let there_are_pending_proofs () = 
-  there_is_a_proof () || 
+let there_are_pending_proofs () =
+  there_is_a_proof () ||
   there_are_suspended_proofs ()
-let check_no_pending_proof () = 
+let check_no_pending_proof () =
   if not (there_are_pending_proofs ()) then
     ()
   else begin
-    Util.error (Pp.string_of_ppcmds
+    Errors.error (Pp.string_of_ppcmds
       (str"Proof editing in progress" ++ (msg_proofs false) ++ fnl() ++
        str"Use \"Abort All\" first or complete proof(s)."))
   end
@@ -196,24 +196,24 @@ let resume id =
   rotate_find id suspended current_proof
 
 let discard_gen id =
-  try 
+  try
     ignore (extract id current_proof);
     remove id proof_info
   with NoSuchProof -> ignore (extract id suspended)
 
-let discard (loc,id) = 
+let discard (loc,id) =
   try
     discard_gen id
   with NoSuchProof ->
-    Util.user_err_loc
+    Errors.user_err_loc
       (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs false)
 
 let discard_current () =
   let (id,_) = extract_top current_proof in
   remove id proof_info
- 
+
 let discard_all () =
-  current_proof := []; 
+  current_proof := [];
   suspended := [];
   proof_info := Idmap.empty
 
@@ -222,7 +222,7 @@ let discard_all () =
 (* Core component.
     No undo handling.
     Applies to proof [id], and proof mode [m]. *)
-let set_proof_mode m id = 
+let set_proof_mode m id =
   let info = Idmap.find id !proof_info in
   let info = { info with mode = m } in
   proof_info := Idmap.add id info !proof_info;
@@ -241,7 +241,7 @@ let set_proof_mode mn =
 
 exception AlreadyExists
 let _ = Errors.register_handler begin function
-  | AlreadyExists -> Util.error "Already editing something of that name."
+  | AlreadyExists -> Errors.error "Already editing something of that name."
   | _ -> raise Errors.Unhandled
 end
 (* [start_proof s str env t hook tac] starts a proof of name [s] and
@@ -259,14 +259,14 @@ let start_proof  id str goals ?(compute_guard=[]) hook =
     end !current_proof
   end;
   let p = Proof.start goals in
-  add id { strength=str ; 
-	        compute_guard=compute_guard ; 
+  add id { strength=str ;
+	        compute_guard=compute_guard ;
 		hook=hook ;
 	        mode = ! default_proof_mode } proof_info ;
   push (id,p) current_proof
 
 (* arnaud: à enlever *)
-let run_tactic tac = 
+let run_tactic tac =
   let p = give_me_the_proof () in
   let env = Global.env () in
   Proof.run_tactic env tac p
@@ -293,7 +293,7 @@ let with_end_tac tac =
 let close_proof () =
   (* spiwack: for now close_proof doesn't actually discard the proof, it is done
       by [Command.save]. *)
-  try 
+  try
     let id = get_current_proof_name () in
     let p = give_me_the_proof () in
     let proofs_and_types = Proof.return p in
@@ -309,11 +309,11 @@ let close_proof () =
       Idmap.find id !proof_info
     in
     (id, (entries,cg,str,hook))
-  with 
+  with
     |  Proof.UnfinishedProof ->
-	 Util.error "Attempt to save an incomplete proof"
+	 Errors.error "Attempt to save an incomplete proof"
     | Proof.HasUnresolvedEvar ->
-	Util.error "Attempt to save a proof with existential variables still non-instantiated"
+	Errors.error "Attempt to save a proof with existential variables still non-instantiated"
 
 
 (**********************************************************)
@@ -392,7 +392,7 @@ module Bullet = struct
 	  while bul <> pop p do () done;
 	  push bul p
 	end
-      else 
+      else
 	push bul p
 
     let strict = {
@@ -404,7 +404,7 @@ module Bullet = struct
 
   (* Current bullet behavior, controled by the option *)
   let current_behavior = ref Strict.strict
-    
+
   let _ =
     Goptions.declare_string_option {Goptions.
       optsync = true;
@@ -428,7 +428,7 @@ module V82 = struct
   let get_current_initial_conclusions () =
     let p = give_me_the_proof () in
     let id = get_current_proof_name () in
-    let { strength=str ; hook=hook } = 
+    let { strength=str ; hook=hook } =
       Idmap.find id !proof_info
     in
     (id,(Proof.V82.get_initial_conclusions p, str, hook))
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index ed6a60c71f..8e09ab9c10 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -35,7 +35,7 @@ val check_no_pending_proof : unit -> unit
 val get_current_proof_name : unit -> Names.identifier
 val get_all_proof_names : unit -> Names.identifier list
 
-val discard : Names.identifier Util.located -> unit
+val discard : Names.identifier Pp.located -> unit
 val discard_current : unit -> unit
 val discard_all : unit -> unit
 
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index e256794a76..876982407f 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -12,7 +12,7 @@ open Evd
 open Names
 open Libnames
 open Term
-open Util
+open Pp
 open Tacexpr
 (* open Decl_expr *)
 open Glob_term
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 2b0a10ba39..10e2ad323a 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -11,7 +11,7 @@ open Evd
 open Names
 open Libnames
 open Term
-open Util
+open Pp
 open Tacexpr
 open Glob_term
 open Genarg
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 4246cc9c7b..ff0e8de413 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -111,7 +111,7 @@ let focus_sublist i j l =
     try 
       Util.list_chop (j-i+1) sub_right 
     with Failure "list_chop" -> 
-      Util.errorlabstrm "nth_unproven" (Pp.str"No such unproven subgoal")
+      Errors.errorlabstrm "nth_unproven" (Pp.str"No such unproven subgoal")
   in
   (sub, (left,right))
 
@@ -280,7 +280,7 @@ let tclFOCUS i j t env = { go = fun sk fk step ->
     is used otherwise. *)
 exception SizeMismatch
 let _ = Errors.register_handler begin function
-  | SizeMismatch -> Util.error "Incorrect number of goals."
+  | SizeMismatch -> Errors.error "Incorrect number of goals."
   | _ -> raise Errors.Unhandled
 end
 (* spiwack: we use an parametrised function to generate the dispatch tacticals.
@@ -316,7 +316,7 @@ let rec tclDISPATCHGEN null join tacs env = { go = fun sk fk step ->
     on with these exceptions. Does not catch anomalies. *)
 let purify t = 
   let t' env = { go = fun sk fk step -> try (t env).go (fun x -> sk (Util.Inl x)) fk step
-     	                                                     with Util.Anomaly _ as e -> raise e
+     	                                                     with Errors.Anomaly _ as e -> raise e
 							           | e -> sk (Util.Inr e) fk step
 	       }
   in
@@ -400,7 +400,7 @@ let rec tclGOALBINDU s k =
 open Pretype_errors
 let rec catchable_exception = function
   | Loc.Exc_located(_,e) -> catchable_exception e
-  | Util.UserError _
+  | Errors.UserError _
   | Type_errors.TypeError _ | PretypeError (_,_,TypingError _)
   | Indrec.RecursionSchemeError _
   | Nametab.GlobalizationError _ | PretypeError (_,_,VarNotFound _)
@@ -505,9 +505,9 @@ module V82 = struct
     let (evk,_) = 
       let evl = Evarutil.non_instantiated pv.solution in
      if (n <= 0) then
-	Util.error "incorrect existential variable index"
+	Errors.error "incorrect existential variable index"
       else if List.length evl < n then
-	  Util.error "not so many uninstantiated existential variables"
+	  Errors.error "not so many uninstantiated existential variables"
       else
 	List.nth evl (n-1) 
     in
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 10e1e66cb2..bddf77d1f4 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Term
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 5cd855476c..19c09571f0 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -8,6 +8,7 @@
 
 open Compat
 open Pp
+open Errors
 open Util
 open Term
 open Termops
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index b8279b8f97..90dddb7486 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -11,6 +11,8 @@ open Topconstr
 open Libnames
 open Nametab
 open Glob_term
+open Errors
+open Pp
 open Util
 open Genarg
 open Pattern
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 5475daa89f..75e9cdf62a 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Namegen
@@ -217,5 +218,5 @@ let pr_gls gls =
 
 let pr_glls glls =
   hov 0 (pr_evar_map (Some 2) (sig_sig glls) ++ fnl () ++
-         prlist_with_sep pr_fnl (db_pr_goal (project glls)) (sig_it glls))
+         prlist_with_sep fnl (db_pr_goal (project glls)) (sig_it glls))
 
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index 62c2359b65..74c8314873 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -78,4 +78,4 @@ val db_logic_failure : debug_info -> exn -> unit
 
 (** Prints a logic failure message for a rule *)
 val db_breakpoint : debug_info ->
-  identifier Util.located message_token list -> unit
+  identifier Pp.located message_token list -> unit