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

12 files changed, 45 insertions, 36 deletions

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