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

30 files changed, 65 insertions, 47 deletions

diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 3266fcf9a..788e664e2 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -14,8 +14,8 @@ open Egrammar
 open Pcoq
 open Compat
 
-let loc = Util.dummy_loc
-let default_loc = <:expr< Util.dummy_loc >>
+let loc = Pp.dummy_loc
+let default_loc = <:expr< Pp.dummy_loc >>
 
 let rec make_rawwit loc = function
   | BoolArgType -> <:expr< Genarg.rawwit_bool >>
@@ -203,8 +203,8 @@ let declare_vernac_argument loc s pr cl =
 	(None, [(None, None, $rules$)]);
       Pptactic.declare_extra_genarg_pprule
         ($rawwit$, $pr_rules$)
-        ($globwit$, fun _ _ _ _ -> Util.anomaly "vernac argument needs not globwit printer")
-        ($wit$, fun _ _ _ _ -> Util.anomaly "vernac argument needs not wit printer") }
+        ($globwit$, fun _ _ _ _ -> Errors.anomaly "vernac argument needs not globwit printer")
+        ($wit$, fun _ _ _ _ -> Errors.anomaly "vernac argument needs not wit printer") }
       >> ]
 
 open Vernacexpr
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 4418a45f7..f30e061ff 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -8,6 +8,7 @@
 
 open Pp
 open Compat
+open Errors
 open Util
 open Pcoq
 open Extend
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index 1d85c74e5..4a5f3c4c6 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -7,7 +7,8 @@
 (************************************************************************)
 
 open Compat
-open Util
+open Errors
+open Pp
 open Names
 open Topconstr
 open Pcoq
diff --git a/parsing/extend.ml b/parsing/extend.ml
index fca24ed5a..22d640f50 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Compat
+open Errors
 open Util
 
 (** Entry keys for constr notations *)
diff --git a/parsing/extrawit.ml b/parsing/extrawit.ml
index ce7346220..cc5b58ee7 100644
--- a/parsing/extrawit.ml
+++ b/parsing/extrawit.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Genarg
 
diff --git a/parsing/extrawit.mli b/parsing/extrawit.mli
index 2d2eef37d..3043fd04b 100644
--- a/parsing/extrawit.mli
+++ b/parsing/extrawit.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Genarg
 open Tacexpr
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index af63e215f..a8adfb19a 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -44,7 +44,7 @@ let mk_fixb (id,bl,ann,body,(loc,tyc)) =
 
 let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
   let _ = Option.map (fun (aloc,_) ->
-    Util.user_err_loc
+    Errors.user_err_loc
       (aloc,"Constr:mk_cofixb",
        Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in
   let ty = match tyc with
@@ -332,7 +332,7 @@ GEXTEND Gram
       [ p = pattern; lp = LIST1 NEXT ->
         (match p with
           | CPatAtom (_, Some r) -> CPatCstr (loc, r, lp)
-          | _ -> Util.user_err_loc
+          | _ -> Errors.user_err_loc
               (cases_pattern_expr_loc p, "compound_pattern",
                Pp.str "Constructor expected."))
       |"@"; r = Prim.reference; lp = LIST1 NEXT ->
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 307e1779e..fd6fc7dd8 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -29,7 +29,7 @@ let my_int_of_string loc s =
     if n > 1024 * 2048 then raise Exit;
     n
   with Failure _ | Exit ->
-    Util.user_err_loc (loc,"",Pp.str "Cannot support a so large number.")
+    Errors.user_err_loc (loc,"",Pp.str "Cannot support a so large number.")
 
 GEXTEND Gram
   GLOBAL:
@@ -94,7 +94,7 @@ GEXTEND Gram
   ;
   ne_string:
     [ [ s = STRING ->
-        if s="" then Util.user_err_loc(loc,"",Pp.str"Empty string."); s
+        if s="" then Errors.user_err_loc(loc,"",Pp.str"Empty string."); s
     ] ]
   ;
   ne_lstring:
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 442aab00e..7d5e976d3 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -8,6 +8,7 @@
 
 open Pp
 open Pcoq
+open Errors
 open Util
 open Tacexpr
 open Glob_term
@@ -117,7 +118,7 @@ let mk_fix_tac (loc,id,bl,ann,ty) =
 
 let mk_cofix_tac (loc,id,bl,ann,ty) =
   let _ = Option.map (fun (aloc,_) ->
-    Util.user_err_loc
+    Errors.user_err_loc
       (aloc,"Constr:mk_cofix_tac",
        Pp.str"Annotation forbidden in cofix expression.")) ann in
   (id,CProdN(loc,bl,ty))
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index a2e053ab8..a52903df0 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -9,6 +9,7 @@
 open Pp
 open Compat
 open Tok
+open Errors
 open Util
 open Names
 open Topconstr
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 1d55a587f..09af49f62 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Term
diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib
index ba393e637..0d7cd3649 100644
--- a/parsing/grammar.mllib
+++ b/parsing/grammar.mllib
@@ -2,13 +2,13 @@ Coq_config
 
 Profile
 Pp_control
-Pp
 Compat
 Flags
+Pp
 Segmenttree
 Unicodetable
-Util
 Errors
+Util
 Bigint
 Dyn
 Hashcons
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
index 1899f7f4d..eda9cea49 100644
--- a/parsing/lexer.mli
+++ b/parsing/lexer.mli
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 
 val add_keyword : string -> unit
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 075440f1c..ee241384b 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -9,6 +9,7 @@
 open Pp
 open Compat
 open Tok
+open Errors
 open Util
 open Names
 open Extend
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index bba0e5602..ebcc53264 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -6,7 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
+open Pp
+open Errors
 open Names
 open Glob_term
 open Extend
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 1f37e36df..20479fe14 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 (*i*)
+open Errors
 open Util
 open Pp
 open Nametab
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index afcdad3e4..c61d4c206 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -14,6 +14,7 @@ open Pcoq
 open Glob_term
 open Topconstr
 open Names
+open Errors
 open Util
 open Genarg
 
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 3305acb77..2f80afdbe 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -9,6 +9,7 @@
 open Pp
 open Names
 open Namegen
+open Errors
 open Util
 open Tacexpr
 open Glob_term
@@ -133,7 +134,7 @@ let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generi
   match Genarg.genarg_tag x with
   | BoolArgType -> str (if out_gen rawwit_bool x then "true" else "false")
   | IntArgType -> int (out_gen rawwit_int x)
-  | IntOrVarArgType -> pr_or_var pr_int (out_gen rawwit_int_or_var x)
+  | IntOrVarArgType -> pr_or_var int (out_gen rawwit_int_or_var x)
   | StringArgType -> str "\"" ++ str (out_gen rawwit_string x) ++ str "\""
   | PreIdentArgType -> str (out_gen rawwit_pre_ident x)
   | IntroPatternArgType -> pr_intro_pattern (out_gen rawwit_intro_pattern x)
@@ -176,7 +177,7 @@ let rec pr_glob_generic prc prlc prtac prpat x =
   match Genarg.genarg_tag x with
   | BoolArgType -> str (if out_gen globwit_bool x then "true" else "false")
   | IntArgType -> int (out_gen globwit_int x)
-  | IntOrVarArgType -> pr_or_var pr_int (out_gen globwit_int_or_var x)
+  | IntOrVarArgType -> pr_or_var int (out_gen globwit_int_or_var x)
   | StringArgType -> str "\"" ++ str (out_gen globwit_string x) ++ str "\""
   | PreIdentArgType -> str (out_gen globwit_pre_ident x)
   | IntroPatternArgType -> pr_intro_pattern (out_gen globwit_intro_pattern x)
@@ -222,7 +223,7 @@ let rec pr_generic prc prlc prtac prpat x =
   match Genarg.genarg_tag x with
   | BoolArgType -> str (if out_gen wit_bool x then "true" else "false")
   | IntArgType -> int (out_gen wit_int x)
-  | IntOrVarArgType -> pr_or_var pr_int (out_gen wit_int_or_var x)
+  | IntOrVarArgType -> pr_or_var int (out_gen wit_int_or_var x)
   | StringArgType -> str "\"" ++ str (out_gen wit_string x) ++ str "\""
   | PreIdentArgType -> str (out_gen wit_pre_ident x)
   | IntroPatternArgType -> pr_intro_pattern (out_gen wit_intro_pattern x)
@@ -423,8 +424,8 @@ let pr_orient b = if b then mt () else str " <-"
 
 let pr_multi = function
   | Precisely 1 -> mt ()
-  | Precisely n -> pr_int n ++ str "!"
-  | UpTo n -> pr_int n ++ str "?"
+  | Precisely n -> int n ++ str "!"
+  | UpTo n -> int n ++ str "?"
   | RepeatStar -> str "?"
   | RepeatPlus -> str "!"
 
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 5a8f2db79..5b8985e9a 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -11,6 +11,7 @@ open Names
 open Nameops
 open Nametab
 open Compat
+open Errors
 open Util
 open Extend
 open Vernacexpr
@@ -928,7 +929,7 @@ let rec pr_vernac = function
   | VernacProof (None, None) -> str "Proof"
   | VernacProof (None, Some l) -> str "Proof using" ++spc()++ prlist pr_lident l
   | VernacProof (Some te, None) -> str "Proof with" ++ spc() ++ pr_raw_tactic te
-  | VernacProof (Some te, Some l) -> 
+  | VernacProof (Some te, Some l) ->
       str "Proof using" ++spc()++ prlist pr_lident l ++ spc() ++
       str "with" ++ spc() ++pr_raw_tactic te
   | VernacProofMode s -> str ("Proof Mode "^s)
@@ -938,7 +939,7 @@ let rec pr_vernac = function
       | Plus -> str"+"
   end ++ spc()
   | VernacSubproof None -> str "BeginSubproof"
-  | VernacSubproof (Some i) -> str "BeginSubproof " ++ pr_int i
+  | VernacSubproof (Some i) -> str "BeginSubproof " ++ int i
   | VernacEndSubproof -> str "EndSubproof"
 
 and pr_extend s cl =
diff --git a/parsing/ppvernac.mli b/parsing/ppvernac.mli
index 6d83ca474..91bb19a8c 100644
--- a/parsing/ppvernac.mli
+++ b/parsing/ppvernac.mli
@@ -12,6 +12,7 @@ open Vernacexpr
 open Names
 open Nameops
 open Nametab
+open Errors
 open Util
 open Ppconstr
 open Pptactic
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index e30979bf9..fad4e879e 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -11,6 +11,7 @@
  *)
 
 open Pp
+open Errors
 open Util
 open Names
 open Nameops
@@ -152,7 +153,7 @@ let print_argument_scopes prefix = function
   | l when not (List.for_all ((=) None) l) ->
      [add_colon prefix ++ hov 2 (str"Argument scopes are" ++ spc() ++
       str "[" ++
-      prlist_with_sep spc (function Some sc -> str sc | None -> str "_") l ++
+      pr_sequence (function Some sc -> str sc | None -> str "_") l ++
       str "]")]
   | _  -> []
 
@@ -168,12 +169,7 @@ let print_simpl_behaviour ref =
      let pp_nomatch = spc() ++ if nomatch then
        str "avoiding to expose match constructs" else str"" in
      let pp_recargs = spc() ++ str "when the " ++
-       let rec aux = function
-         | [] -> mt()
-         | [x] -> str (ordinal (x+1))
-         | [x;y] -> str (ordinal (x+1)) ++ str " and " ++ str (ordinal (y+1))
-         | x::tl -> str (ordinal (x+1)) ++ str ", " ++ aux tl in
-       aux recargs ++ str (plural (List.length recargs) " argument") ++
+       pr_enum (fun x -> pr_nth (x+1)) recargs ++ str (plural (List.length recargs) " argument") ++
        str (plural (if List.length recargs >= 2 then 1 else 2) " evaluate") ++
        str " to a constructor" in
      let pp_nargs =
@@ -722,13 +718,13 @@ let print_path ((i,j),p) =
 let _ = Classops.install_path_printer print_path
 
 let print_graph () =
-  prlist_with_sep pr_fnl print_path (inheritance_graph())
+  prlist_with_sep fnl print_path (inheritance_graph())
 
 let print_classes () =
-  prlist_with_sep pr_spc pr_class (classes())
+  pr_sequence pr_class (classes())
 
 let print_coercions () =
-  prlist_with_sep pr_spc print_coercion_value (coercions())
+  pr_sequence print_coercion_value (coercions())
 
 let index_of_class cl =
   try
@@ -751,7 +747,7 @@ let print_path_between cls clt =
   print_path ((i,j),p)
 
 let print_canonical_projections () =
-  prlist_with_sep pr_fnl
+  prlist_with_sep fnl
     (fun ((r1,r2),o) -> pr_cs_pattern r2 ++
     str " <- " ++
     pr_global r1 ++ str " ( " ++ pr_lconstr o.o_DEF ++ str " )")
diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli
index 6d9c6ecc6..40ba7f047 100644
--- a/parsing/prettyp.mli
+++ b/parsing/prettyp.mli
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Sign
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 0a3926660..3d2f3e089 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Nameops
@@ -505,17 +506,17 @@ let pr_prim_rule = function
        ++ pr_id id ++ str" (type of "  ++ pr_id id ++ str ")")
 
   | Thin ids ->
-      (str"clear "  ++ prlist_with_sep pr_spc pr_id ids)
+      (str"clear "  ++ pr_sequence pr_id ids)
 
   | ThinBody ids ->
-      (str"clearbody "  ++ prlist_with_sep pr_spc pr_id ids)
+      (str"clearbody "  ++ pr_sequence pr_id ids)
 
   | Move (withdep,id1,id2) ->
       (str (if withdep then "dependent " else "") ++
 	 str"move "  ++ pr_id id1 ++ pr_move_location pr_id id2)
 
   | Order ord ->
-      (str"order "  ++ prlist_with_sep pr_spc pr_id ord)
+      (str"order "  ++ pr_sequence pr_id ord)
 
   | Rename (id1,id2) ->
       (str "rename " ++ pr_id id1 ++ str " into " ++ pr_id id2)
diff --git a/parsing/printmod.ml b/parsing/printmod.ml
index 9cf76585e..cf047bfa3 100644
--- a/parsing/printmod.ml
+++ b/parsing/printmod.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Declarations
diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4
index 605432692..5bd215190 100644
--- a/parsing/q_constr.ml4
+++ b/parsing/q_constr.ml4
@@ -13,13 +13,13 @@ open Term
 open Names
 open Pattern
 open Q_util
-open Util
+open Pp
 open Compat
 open Pcaml
 open PcamlSig
 
 let loc = dummy_loc
-let dloc = <:expr< Util.dummy_loc >>
+let dloc = <:expr< Pp.dummy_loc >>
 
 let apply_ref f l =
   <:expr<
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 552c86903..389118c34 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
+open Pp
 open Names
 open Libnames
 open Q_util
@@ -24,7 +24,7 @@ let anti loc x =
 (* We don't give location for tactic quotation! *)
 let loc = dummy_loc
 
-let dloc = <:expr< Util.dummy_loc >>
+let dloc = <:expr< Pp.dummy_loc >>
 
 let mlexpr_of_ident id =
   <:expr< Names.id_of_string $str:Names.string_of_id id$ >>
diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4
index 91ab29f1d..cfaa2a654 100644
--- a/parsing/q_util.ml4
+++ b/parsing/q_util.ml4
@@ -10,7 +10,7 @@
 
 open Extrawit
 open Compat
-open Util
+open Pp
 
 let mlexpr_of_list f l =
   List.fold_right
@@ -64,6 +64,6 @@ let rec mlexpr_of_prod_entry_key = function
   | Pcoq.Aself -> <:expr< Pcoq.Aself >>
   | Pcoq.Anext -> <:expr< Pcoq.Anext >>
   | Pcoq.Atactic n -> <:expr< Pcoq.Atactic $mlexpr_of_int n$ >>
-  | Pcoq.Agram s -> Util.anomaly "Agram not supported"
+  | Pcoq.Agram s -> Errors.anomaly "Agram not supported"
   | Pcoq.Aentry ("",s) -> <:expr< Pcoq.Agram (Pcoq.Gram.Entry.obj $lid:s$) >>
   | Pcoq.Aentry (u,s) -> <:expr< Pcoq.Aentry $str:u$ $str:s$ >>
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index 2fe1fdda7..838c771c6 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -9,6 +9,7 @@
 (*i camlp4deps: "tools/compat5b.cmo" i*)
 
 open Util
+open Pp
 open Genarg
 open Q_util
 open Q_coqast
@@ -196,7 +197,7 @@ EXTEND
         let t, g = interp_entry_name false None e sep in
         GramNonTerminal (loc, t, g, Some (Names.id_of_string s))
       | s = STRING ->
-	if s = "" then Util.user_err_loc (loc,"",Pp.str "Empty terminal.");
+	if s = "" then Errors.user_err_loc (loc,"",Pp.str "Empty terminal.");
         GramTerminal s
     ] ]
   ;
diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml
index 83dae3dce..b2b59f166 100644
--- a/parsing/tactic_printer.ml
+++ b/parsing/tactic_printer.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Sign
 open Evd
@@ -66,7 +67,7 @@ let rec print_proof sigma osign pf =
 	   spc () ++ str" BY " ++
 	   hov 0 (pr_rule r) ++ fnl () ++
 	   str"  " ++
-	   hov 0 (prlist_with_sep pr_fnl (print_proof sigma hyps) spfl))
+	   hov 0 (prlist_with_sep fnl (print_proof sigma hyps) spfl))
 
 let pr_change sigma gl =
   str"change " ++
@@ -110,11 +111,11 @@ let print_script ?(nochange=true) sigma pf =
 	  end
     | Some(Daimon,spfl) ->
 	((if nochange then (mt ()) else (pr_change sigma pf.goal ++ fnl ())) ++
-	   prlist_with_sep pr_fnl print_prf spfl )
+	   prlist_with_sep fnl print_prf spfl )
     | Some(rule,spfl) ->
 	((if nochange then (mt ()) else (pr_change sigma pf.goal ++ fnl ())) ++
 	   pr_rule_dot_fnl rule ++
-	   prlist_with_sep pr_fnl print_prf spfl ) in
+	   prlist_with_sep fnl print_prf spfl ) in
   print_prf pf
 
 (* printed by Show Script command *)
@@ -140,7 +141,7 @@ let print_treescript ?(nochange=true) sigma pf =
 	end
     | Some(Daimon,spfl) ->
 	(if nochange then mt () else pr_change sigma pf.goal ++ fnl ()) ++
-	prlist_with_sep pr_fnl (print_script ~nochange sigma) spfl
+	prlist_with_sep fnl (print_script ~nochange sigma) spfl
     | Some(r,spfl) ->
         let indent = if List.length spfl >= 2 then 1 else 0 in
         (if nochange then mt () else pr_change sigma pf.goal ++ fnl ()) ++
@@ -162,7 +163,7 @@ let rec print_info_script sigma osign pf =
 		      print_info_script sigma
 		      (Environ.named_context_of_val sign) pf1)
              | _ -> (str"." ++ fnl () ++
-                       prlist_with_sep pr_fnl
+                       prlist_with_sep fnl
                          (print_info_script sigma
 			    (Environ.named_context_of_val sign)) spfl))
 
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index 88a750792..7553aef4a 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -8,6 +8,7 @@
 
 (*i camlp4deps: "tools/compat5b.cmo" i*)
 
+open Pp
 open Util
 open Genarg
 open Q_util
@@ -79,7 +80,7 @@ EXTEND
   rule:
     [ [ "["; s = STRING; l = LIST0 args; "]"; "->"; "["; e = Pcaml.expr; "]"
         ->
-      if s = "" then Util.user_err_loc (loc,"",Pp.str"Command name is empty.");
+      if s = "" then Errors.user_err_loc (loc,"",Pp.str"Command name is empty.");
       (Some s,l,<:expr< fun () -> $e$ >>)
       | "[" ; "-" ; l = LIST1 args ; "]" ; "->" ; "[" ; e = Pcaml.expr ; "]" ->
 	  (None,l,<:expr< fun () -> $e$ >>)