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

37 files changed, 60 insertions, 31 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 93ca89f47..c650565c0 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Nameops
@@ -268,7 +269,7 @@ let path_derivate hp hint = normalize_path (path_derivate hp hint)
 
 let rec pp_hints_path = function
   | PathAtom (PathAny) -> str"."
-  | PathAtom (PathHints grs) -> prlist_with_sep pr_spc pr_global grs
+  | PathAtom (PathHints grs) -> pr_sequence pr_global grs
   | PathStar p -> str "(" ++ pp_hints_path p ++ str")*"
   | PathSeq (p, p') -> pp_hints_path p ++ str" ; " ++ pp_hints_path p'
   | PathOr (p, p') -> 
@@ -960,7 +961,7 @@ let print_applicable_hint () =
   let pts = get_pftreestate () in
   let glss = Proof.V82.subgoals pts in
   match glss.Evd.it with
-  | [] -> Util.error "No focused goal."
+  | [] -> Errors.error "No focused goal."
   | g::_ ->
     let gl = { Evd.it = g; sigma = glss.Evd.sigma } in
     print_hint_term (pf_concl gl)
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 521c5ed24..bd425c1de 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Names
 open Term
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index a974c76a0..990da9306 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -16,6 +16,7 @@ open Tacinterp
 open Tactics
 open Term
 open Termops
+open Errors
 open Util
 open Glob_term
 open Vernacinterp
@@ -203,7 +204,7 @@ let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl gl =
 	*)
 	gen_auto_multi_rewrite conds tac_main lbas cl gl
     | _ ->
-	    Util.errorlabstrm "autorewrite"
+	    Errors.errorlabstrm "autorewrite"
 	      (strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion.")
 
 (* Functions necessary to the library object declaration *)
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index 3205b0418..6481217b6 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -12,7 +12,7 @@ open Tacmach
 open Equality
 
 (** Rewriting rules before tactic interpretation *)
-type raw_rew_rule = Util.loc * Term.constr * bool * Tacexpr.raw_tactic_expr
+type raw_rew_rule = Pp.loc * Term.constr * bool * Tacexpr.raw_tactic_expr
 
 (** To add rewriting rules to a base *)
 val add_rew_rules : string -> raw_rew_rule list -> unit
@@ -56,6 +56,6 @@ type hypinfo = {
 }
 
 val find_applied_relation : bool ->
-  Util.loc ->
+  Pp.loc ->
   Environ.env -> Evd.evar_map -> Term.constr -> bool -> hypinfo
 
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 42df244de..4a850db66 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -9,6 +9,7 @@
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
 open Pp
+open Errors
 open Util
 open Names
 open Nameops
@@ -212,7 +213,7 @@ let nb_empty_evars s =
 
 let pr_ev evs ev = Printer.pr_constr_env (Goal.V82.env evs ev) (Evarutil.nf_evar evs (Goal.V82.concl evs ev))
 
-let pr_depth l = prlist_with_sep (fun () -> str ".") pr_int (List.rev l)
+let pr_depth l = prlist_with_sep (fun () -> str ".") int (List.rev l)
 
 type autoinfo = { hints : Auto.hint_db; is_evar: existential_key option;
 		  only_classes: bool; auto_depth: int list; auto_last_tac: std_ppcmds Lazy.t;
@@ -744,7 +745,7 @@ ARGUMENT EXTEND debug TYPED AS bool PRINTED BY pr_debug
 END
 
 let pr_depth _prc _prlc _prt = function
-    Some i -> Util.pr_int i
+    Some i -> Pp.int i
   | None -> Pp.mt()
 
 ARGUMENT EXTEND depth TYPED AS int option PRINTED BY pr_depth
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index a3d43623e..f8cca076f 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -6,7 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
+open Pp
+open Errors
 open Term
 open Proof_type
 open Hipattern
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index fd924707c..e7c4e0676 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -110,6 +110,7 @@ Qed.
 *)
 
 open Pp
+open Errors
 open Util
 open Names
 open Term
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 9966fb772..4923aa720 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -9,6 +9,7 @@
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
 open Pp
+open Errors
 open Util
 open Names
 open Nameops
@@ -505,7 +506,7 @@ let pr_hints_path_atom prc _ _ a =
   match a with
   | PathAny -> str"."
   | PathHints grs ->
-    prlist_with_sep pr_spc Printer.pr_global grs
+    pr_sequence Printer.pr_global grs
 
 ARGUMENT EXTEND hints_path_atom
   TYPED AS hints_path_atom
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 1ff8800f1..aa13d27b1 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Term
diff --git a/tactics/elim.mli b/tactics/elim.mli
index 48a7ca68c..c40d1cbbc 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -19,7 +19,7 @@ val introElimAssumsThen :
   (branch_assumptions -> tactic) -> branch_args -> tactic
 
 val introCaseAssumsThen :
-  (intro_pattern_expr Util.located list -> branch_assumptions -> tactic) ->
+  (intro_pattern_expr Pp.located list -> branch_assumptions -> tactic) ->
     branch_args -> tactic
 
 val general_decompose : (identifier * constr -> bool) -> constr -> tactic
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index 6d40b2daf..1a65f6278 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -14,6 +14,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
+open Errors
 open Util
 open Names
 open Namegen
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 779fe265b..fe380db7c 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -44,6 +44,7 @@
    natural expectation of the user.
 *)
 
+open Errors
 open Util
 open Names
 open Term
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 10fd0fef9..e3b62e496 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Nameops
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 790594699..12deb7d32 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 (*i*)
+open Pp
 open Util
 open Names
 open Term
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 992fdc915..f1341762a 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -7,7 +7,8 @@
 (************************************************************************)
 
 open Term
-open Util
+open Pp
+open Errors
 open Evar_refiner
 open Tacmach
 open Tacexpr
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 6a13ac2a9..0496d758b 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -127,7 +127,7 @@ END
 
 type 'id gen_place= ('id * hyp_location_flag,unit) location
 
-type loc_place = identifier Util.located gen_place
+type loc_place = identifier Pp.located gen_place
 type place = identifier gen_place
 
 let pr_gen_place pr_id = function
@@ -166,11 +166,11 @@ ARGUMENT EXTEND hloc
   |  [ "in" "|-" "*" ] ->
     [ ConclLocation () ]
 | [ "in" ident(id) ] ->
-    [ HypLocation ((Util.dummy_loc,id),InHyp) ]
+    [ HypLocation ((Pp.dummy_loc,id),InHyp) ]
 | [ "in" "(" "Type" "of" ident(id) ")" ] ->
-    [ HypLocation ((Util.dummy_loc,id),InHypTypeOnly) ]
+    [ HypLocation ((Pp.dummy_loc,id),InHypTypeOnly) ]
 | [ "in" "(" "Value" "of" ident(id) ")" ] ->
-    [ HypLocation ((Util.dummy_loc,id),InHypValueOnly) ]
+    [ HypLocation ((Pp.dummy_loc,id),InHypValueOnly) ]
 
  END
 
@@ -203,7 +203,7 @@ let pr_in_hyp  pr_id (lo,concl) :  Pp.std_ppcmds =
     | None,false -> str "in" ++ spc () ++ str "*" ++ spc () ++ str "|-"
     | Some l,_ ->
 	str "in" ++
-	  Util.prlist (fun id -> spc () ++ pr_id id) l ++
+	  pr_sequence pr_id l ++
 	  match concl with
 	    | true -> spc () ++ str "|-" ++ spc () ++ str "*"
 	    | _ -> mt ()
@@ -214,7 +214,7 @@ let pr_in_arg_hyp _ _ _ = pr_in_hyp (fun (_,id) -> Ppconstr.pr_id id)
 let pr_in_arg_hyp_typed  _ _  _  = pr_in_hyp Ppconstr.pr_id
 
 
-let pr_var_list_gen pr_id = Util.prlist_with_sep (fun () -> str ",") pr_id
+let pr_var_list_gen pr_id = Pp.prlist_with_sep (fun () -> str ",") pr_id
 
 let pr_var_list_typed _ _ _ =  pr_var_list_gen Ppconstr.pr_id
 
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index 2abca40eb..a682af04f 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -30,7 +30,7 @@ val glob : constr_expr Pcoq.Gram.entry
 
 type 'id gen_place= ('id * hyp_location_flag,unit) location
 
-type loc_place = identifier Util.located gen_place
+type loc_place = identifier Pp.located gen_place
 type place = identifier gen_place
 
 val rawwit_hloc : loc_place raw_abstract_argument_type
@@ -38,10 +38,10 @@ val wit_hloc : place typed_abstract_argument_type
 val hloc : loc_place Pcoq.Gram.entry
 val pr_hloc : loc_place -> Pp.std_ppcmds
 
-val in_arg_hyp:  (Names.identifier Util.located list option * bool)  Pcoq.Gram.entry
-val rawwit_in_arg_hyp : (Names.identifier Util.located list option * bool) raw_abstract_argument_type
+val in_arg_hyp:  (Names.identifier Pp.located list option * bool)  Pcoq.Gram.entry
+val rawwit_in_arg_hyp : (Names.identifier Pp.located list option * bool) raw_abstract_argument_type
 val wit_in_arg_hyp : (Names.identifier list option * bool) typed_abstract_argument_type
-val raw_in_arg_hyp_to_clause : (Names.identifier Util.located list option * bool) -> Tacticals.clause
+val raw_in_arg_hyp_to_clause : (Names.identifier Pp.located list option * bool) -> Tacticals.clause
 val glob_in_arg_hyp_to_clause :  (Names.identifier list option * bool)  -> Tacticals.clause
 val pr_in_arg_hyp : (Names.identifier list option * bool) -> Pp.std_ppcmds
 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 44a3b0173..9c0d5db2c 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -17,6 +17,7 @@ open Names
 open Tacexpr
 open Glob_term
 open Tactics
+open Errors
 open Util
 open Evd
 open Equality
@@ -60,7 +61,7 @@ END
 
 let induction_arg_of_quantified_hyp = function
   | AnonHyp n -> ElimOnAnonHyp n
-  | NamedHyp id -> ElimOnIdent (Util.dummy_loc,id)
+  | NamedHyp id -> ElimOnIdent (Pp.dummy_loc,id)
 
 (* Versions *_main must come first!! so that "1" is interpreted as a
    ElimOnAnonHyp and not as a "constr", and "id" is interpreted as a
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index fafc681ae..302bde6e6 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -62,10 +62,10 @@ let h_generalize cl =
 let h_generalize_dep c =
   abstract_tactic (TacGeneralizeDep c) (generalize_dep c)
 let h_let_tac b na c cl =
-  let with_eq = if b then None else Some (true,(dummy_loc,IntroAnonymous)) in
+  let with_eq = if b then None else Some (true,(Pp.dummy_loc,IntroAnonymous)) in
   abstract_tactic (TacLetTac (na,c,cl,b)) (letin_tac with_eq na c None cl)
 let h_let_pat_tac b na c cl =
-  let with_eq = if b then None else Some (true,(dummy_loc,IntroAnonymous)) in
+  let with_eq = if b then None else Some (true,(Pp.dummy_loc,IntroAnonymous)) in
   abstract_tactic (TacLetTac (na,snd c,cl,b))
     (letin_pat_tac with_eq na c None cl)
 
@@ -130,8 +130,8 @@ let h_transitivity c =
   abstract_tactic (TacTransitivity c)
     (intros_transitivity c)
 
-let h_simplest_apply c = h_apply false false [dummy_loc,(c,NoBindings)]
-let h_simplest_eapply c = h_apply false true [dummy_loc,(c,NoBindings)]
+let h_simplest_apply c = h_apply false false [Pp.dummy_loc,(c,NoBindings)]
+let h_simplest_eapply c = h_apply false true [Pp.dummy_loc,(c,NoBindings)]
 let h_simplest_elim c   = h_elim false (c,NoBindings) None
 let h_simplest_case   c = h_case false (c,NoBindings)
 
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 96e7e3f03..ca683cc24 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Util
+open Pp
 open Term
 open Proof_type
 open Tacmach
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index 9057c60d3..6f07eed70 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -9,6 +9,7 @@
 (*i camlp4deps: "parsing/grammar.cma parsing/q_constr.cmo" i*)
 
 open Pp
+open Errors
 open Util
 open Names
 open Nameops
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index aa3863649..82e9e3b8e 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Names
 open Term
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 2ae4e22e5..47e50d832 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Nameops
diff --git a/tactics/inv.mli b/tactics/inv.mli
index ef828d882..a7e70dd0d 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
+open Pp
 open Names
 open Term
 open Tacmach
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 1697c1465..33f8c9eef 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Nameops
diff --git a/tactics/leminv.mli b/tactics/leminv.mli
index 233aeba3a..d5deff1f5 100644
--- a/tactics/leminv.mli
+++ b/tactics/leminv.mli
@@ -1,4 +1,4 @@
-open Util
+open Pp
 open Names
 open Term
 open Glob_term
diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml
index 4e34fae84..dce518f87 100644
--- a/tactics/nbtermdn.ml
+++ b/tactics/nbtermdn.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Names
 open Term
diff --git a/tactics/refine.ml b/tactics/refine.ml
index e7f3998aa..fa023e78e 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -47,6 +47,7 @@
  *)
 
 open Pp
+open Errors
 open Util
 open Names
 open Term
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index ef3ec1470..b8bd166b9 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -9,6 +9,7 @@
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
 open Pp
+open Errors
 open Util
 open Names
 open Nameops
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index e2a99707f..d4a7be4ec 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -18,6 +18,7 @@ open Pp
 open Glob_term
 open Sign
 open Tacred
+open Errors
 open Util
 open Names
 open Nameops
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index d9dc8094f..4d01e5ad9 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Proof_type
@@ -102,7 +103,7 @@ val intern_constr_with_bindings :
   glob_constr_and_expr * glob_constr_and_expr Glob_term.bindings
 
 val intern_hyp :
-  glob_sign -> identifier Util.located -> identifier Util.located
+  glob_sign -> identifier Pp.located -> identifier Pp.located
 
 val subst_genarg :
   substitution -> glob_generic_argument -> glob_generic_argument
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 11625cbdf..2bb9c1cbe 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Term
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index db9ab0c9b..42c70eef4 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Term
@@ -170,7 +171,7 @@ type branch_assumptions = {
 (** [check_disjunctive_pattern_size loc pats n] returns an appropriate 
    error message if |pats| <> n *)
 val check_or_and_pattern_size :
-  Util.loc -> or_and_intro_pattern_expr -> int -> unit
+  Pp.loc -> or_and_intro_pattern_expr -> int -> unit
 
 (** Tolerate "[]" to mean a disjunctive pattern of any length *)
 val fix_empty_or_and_pattern : int -> or_and_intro_pattern_expr ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 11b0b9b81..0f23d512f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -8,6 +8,7 @@
 
 open Compat
 open Pp
+open Errors
 open Util
 open Names
 open Nameops
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index f8f32b792..6e3c2cff4 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Pp
 open Util
 open Names
 open Term
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index b7a58be45..c953bedcb 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -17,6 +17,7 @@ open Proof_type
 open Tacticals
 open Tacinterp
 open Tactics
+open Errors
 open Util
 open Genarg
 
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index 443acc6f5..5f6e5580e 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Names
 open Nameops