Added an indirection with respect to Loc in Compat. As many [open Compat]

were closed (i.e. the only remaining ones are those of printing/parsing).
Meanwhile, a simplified interface is provided in loc.mli.

This also permits to put Pp in Clib, because it does not depend on
CAMLP4/5 anymore.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 9 insertions, 7 deletions

diff --git a/library/declaremods.mli b/library/declaremods.mli
index 800e2eaa8..3064564ca 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Loc
 open Pp
 open Names
 open Entries
diff --git a/library/lib.mli b/library/lib.mli
index 318997067..382637e9e 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -161,7 +161,7 @@ val first_command_label : int
 val reset_label : int -> unit
 
 (** search the label registered immediately before adding some definition *)
-val label_before_name : Names.identifier Pp.located -> int
+val label_before_name : Names.identifier Loc.located -> int
 
 (** {6 We can get and set the state of the operations (used in [States]). } *)
 
diff --git a/library/libnames.ml b/library/libnames.ml
index 37ae97ace..f3e8d17f3 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -153,8 +153,8 @@ type global_dir_reference =
       (* this won't last long I hope! *)
 
 type reference =
-  | Qualid of qualid located
-  | Ident of identifier located
+  | Qualid of qualid Loc.located
+  | Ident of identifier Loc.located
 
 let qualid_of_reference = function
   | Qualid (loc,qid) -> loc, qid
diff --git a/library/libnames.mli b/library/libnames.mli
index 24bdd2048..227d1f3df 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Loc
 open Names
 
 (** {6 Dirpaths } *)
@@ -109,7 +110,7 @@ type reference =
 val qualid_of_reference : reference -> qualid located
 val string_of_reference : reference -> string
 val pr_reference : reference -> std_ppcmds
-val loc_of_reference : reference -> loc
+val loc_of_reference : reference -> Loc.t
 
 (** Deprecated synonyms *)
 
diff --git a/library/library.mli b/library/library.mli
index 766e22afa..a19149332 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Loc
 open Pp
 open Names
 open Libnames
diff --git a/library/nametab.ml b/library/nametab.ml
index 2bdd71cc4..84f6c6542 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -8,7 +8,6 @@
 
 open Errors
 open Util
-open Compat
 open Pp
 open Names
 open Libnames
diff --git a/library/nametab.mli b/library/nametab.mli
index 871ed6676..b82ad0175 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -61,9 +61,9 @@ exception GlobalizationError of qualid
 exception GlobalizationConstantError of qualid
 
 (** Raises a globalization error *)
-val error_global_not_found_loc : loc -> qualid -> 'a
+val error_global_not_found_loc : Loc.t -> qualid -> 'a
 val error_global_not_found     : qualid -> 'a
-val error_global_constant_not_found_loc : loc -> qualid -> 'a
+val error_global_constant_not_found_loc : Loc.t -> qualid -> 'a
 
 (** {6 Register visibility of things } *)