24 files changed, 43 insertions, 27 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index f7bd328154..1ffa2c486f 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -8,6 +8,7 @@
 
 (*i*)
 open Pp
+open Errors
 open Util
 open Univ
 open Names
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 2a53eb85fe..c112506ab1 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
+open Pp
 open Names
 open Term
 open Termops
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 04e252ca37..c94ac67ded 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Flags
 open Names
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index eb7828eaa6..9eda0b96a9 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Pp
 open Names
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 5d3580f26a..27137e81bd 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -11,6 +11,7 @@ open Libnames
 open Nametab
 open Term
 open Pattern
+open Errors
 open Util
 
 (** This module collects the global references, constructions and
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 07e813e743..5ea9cb986d 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -124,7 +124,7 @@ let remove_sections dir =
     dir
 
 let interval loc =
-  let loc1,loc2 = Util.unloc loc in
+  let loc1,loc2 = Pp.unloc loc in
   loc1, loc2-1
 
 let dump_ref loc filepath modpath ident ty =
@@ -143,7 +143,7 @@ let add_glob_gen loc sp lib_dp ty =
       dump_ref loc filepath modpath ident ty
 
 let add_glob loc ref =
-  if dump () && loc <> Util.dummy_loc then
+  if dump () && loc <> Pp.dummy_loc then
     let sp = Nametab.path_of_global ref in
     let lib_dp = Lib.library_part ref in
     let ty = type_of_global_ref ref in
@@ -154,7 +154,7 @@ let mp_of_kn kn =
     Names.MPdot (mp,l)
 
 let add_glob_kn loc kn =
-  if dump () && loc <> Util.dummy_loc then
+  if dump () && loc <> Pp.dummy_loc then
     let sp = Nametab.path_of_syndef kn in
     let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in
       add_glob_gen loc sp lib_dp "syndef"
@@ -237,7 +237,7 @@ let cook_notation df sc =
 
 let dump_notation (loc,(df,_)) sc sec =
   (* We dump the location of the opening '"' *)
-  dump_string (Printf.sprintf "not %d %s %s\n" (fst (Util.unloc loc))
+  dump_string (Printf.sprintf "not %d %s %s\n" (fst (Pp.unloc loc))
     (Names.string_of_dirpath (Lib.current_dirpath sec)) (cook_notation df sc))
 
 let dump_notation_location posl df (((path,secpath),_),sc) =
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index b02cc9669f..90b56e0a99 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -26,17 +26,17 @@ type coqdoc_state = Lexer.location_table
 val coqdoc_freeze : unit -> coqdoc_state
 val coqdoc_unfreeze : coqdoc_state -> unit
 
-val add_glob : Util.loc -> Libnames.global_reference -> unit
-val add_glob_kn : Util.loc -> Names.kernel_name -> unit
-
-val dump_definition : Util.loc * Names.identifier -> bool -> string -> unit
-val dump_moddef : Util.loc -> Names.module_path -> string -> unit
-val dump_modref  : Util.loc -> Names.module_path -> string -> unit
-val dump_reference  : Util.loc -> string -> string -> string -> unit
-val dump_libref : Util.loc -> Names.dir_path -> string -> unit
+val add_glob : Pp.loc -> Libnames.global_reference -> unit
+val add_glob_kn : Pp.loc -> Names.kernel_name -> unit
+
+val dump_definition : Pp.loc * Names.identifier -> bool -> string -> unit
+val dump_moddef : Pp.loc -> Names.module_path -> string -> unit
+val dump_modref  : Pp.loc -> Names.module_path -> string -> unit
+val dump_reference  : Pp.loc -> string -> string -> string -> unit
+val dump_libref : Pp.loc -> Names.dir_path -> string -> unit
 val dump_notation_location : (int * int) list -> Topconstr.notation -> (Notation.notation_location * Topconstr.scope_name option) -> unit
-val dump_binding : Util.loc -> Names.Idset.elt -> unit
-val dump_notation : Util.loc * (Topconstr.notation * Notation.notation_location) -> Topconstr.scope_name option -> bool -> unit
+val dump_binding : Pp.loc -> Names.Idset.elt -> unit
+val dump_notation : Pp.loc * (Topconstr.notation * Notation.notation_location) -> Topconstr.scope_name option -> bool -> unit
 val dump_constraint :  Topconstr.typeclass_constraint -> bool -> string -> unit
 
 val dump_string : string -> unit
diff --git a/interp/genarg.ml b/interp/genarg.ml
index e564bd11e1..b4f87d96b3 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Nameops
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 54aadba187..9c47c691a9 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -6,7 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
+open Errors
+open Pp
 open Names
 open Term
 open Libnames
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index f273904353..e92699f646 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -15,6 +15,7 @@ open Evd
 open Environ
 open Nametab
 open Mod_subst
+open Errors
 open Util
 open Glob_term
 open Topconstr
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index ce518a9cb3..14a1c630c5 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -16,7 +16,7 @@ open Nametab
 open Mod_subst
 open Glob_term
 open Topconstr
-open Util
+open Pp
 open Libnames
 open Typeclasses
 
diff --git a/interp/modintern.ml b/interp/modintern.ml
index a13560c0ff..5dde644b5b 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Entries
diff --git a/interp/modintern.mli b/interp/modintern.mli
index 71a00c2fef..e808cd9805 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.mli
@@ -9,7 +9,7 @@
 open Declarations
 open Environ
 open Entries
-open Util
+open Pp
 open Libnames
 open Names
 open Topconstr
diff --git a/interp/notation.ml b/interp/notation.ml
index 8f19ab851f..96de08da3a 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 (*i*)
+open Errors
 open Util
 open Pp
 open Bigint
diff --git a/interp/notation.mli b/interp/notation.mli
index f92ef94ed3..25ea594190 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Pp
 open Bigint
diff --git a/interp/ppextend.ml b/interp/ppextend.ml
index ebf94bd80b..176c2a76b3 100644
--- a/interp/ppextend.ml
+++ b/interp/ppextend.ml
@@ -8,6 +8,7 @@
 
 (*i*)
 open Pp
+open Errors
 open Util
 open Names
 (*i*)
diff --git a/interp/reserve.ml b/interp/reserve.ml
index a07f5c8463..7f30c6bacd 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -8,6 +8,7 @@
 
 (* Reserved names *)
 
+open Errors
 open Util
 open Pp
 open Names
diff --git a/interp/reserve.mli b/interp/reserve.mli
index 97b22d2b22..f3b9d43a55 100644
--- a/interp/reserve.mli
+++ b/interp/reserve.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
+open Pp
 open Names
 open Glob_term
 open Topconstr
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 4e472b7a53..043c255a47 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -13,6 +13,7 @@
 
 (* *)
 open Pp
+open Errors
 open Util
 open Names
 open Libnames
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
index 474058cc9f..0c7bc6157e 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
+open Pp
 open Names
 open Libnames
 open Genarg
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 8863bbbd3b..eb6f50131f 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Pp
 open Names
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index e4da52a331..9e15ab970e 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Names
 open Topconstr
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index b2e1a75457..ca17060357 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -8,6 +8,7 @@
 
 (*i*)
 open Pp
+open Errors
 open Util
 open Names
 open Nameops
@@ -857,7 +858,7 @@ type cases_pattern_expr =
   | CPatOr of loc * cases_pattern_expr list
   | CPatNotation of loc * notation * cases_pattern_notation_substitution
   | CPatPrim of loc * prim_token
-  | CPatRecord of Util.loc * (reference * cases_pattern_expr) list
+  | CPatRecord of loc * (reference * cases_pattern_expr) list
   | CPatDelimiters of loc * string * cases_pattern_expr
 
 and cases_pattern_notation_substitution =
@@ -1272,8 +1273,8 @@ type module_ast =
 (* and which are then occupied by proper symbols of the notation (or spaces) *)
 
 let locs_of_notation loc locs ntn =
-  let (bl,el) = Util.unloc loc in
-  let locs =  List.map Util.unloc locs in
+  let (bl,el) = unloc loc in
+  let locs =  List.map unloc locs in
   let rec aux pos = function
     | [] -> if pos = el then [] else [(pos,el-1)]
     | (ba,ea)::l ->if pos = ba then aux ea l else (pos,ba-1)::aux ea l
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 5ee0c5bc62..ea31917701 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Util
+open Errors
 open Names
 open Libnames
 open Glob_term
@@ -130,7 +130,7 @@ type cases_pattern_expr =
   | CPatOr of loc * cases_pattern_expr list
   | CPatNotation of loc * notation * cases_pattern_notation_substitution
   | CPatPrim of loc * prim_token
-  | CPatRecord of Util.loc * (reference * cases_pattern_expr) list
+  | CPatRecord of loc * (reference * cases_pattern_expr) list
   | CPatDelimiters of loc * string * cases_pattern_expr
 
 and cases_pattern_notation_substitution =
@@ -267,6 +267,6 @@ type module_ast =
   | CMwith of loc * module_ast * with_declaration_ast
 
 val ntn_loc :
-  Util.loc -> constr_notation_substitution -> string -> (int * int) list
+  loc -> constr_notation_substitution -> string -> (int * int) list
 val patntn_loc :
-  Util.loc -> cases_pattern_notation_substitution -> string -> (int * int) list
+  loc -> cases_pattern_notation_substitution -> string -> (int * int) list