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

1 files changed, 10 insertions, 10 deletions

diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 469df12224..73354fa404 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -22,19 +22,19 @@ val dump_to_dotglob : unit -> unit
 val pause : unit -> unit
 val continue : unit -> unit
 
-val add_glob : Pp.loc -> Globnames.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 add_glob : Loc.t -> Globnames.global_reference -> unit
+val add_glob_kn : Loc.t -> Names.kernel_name -> unit
+
+val dump_definition : Loc.t * Names.identifier -> bool -> string -> unit
+val dump_moddef : Loc.t -> Names.module_path -> string -> unit
+val dump_modref  : Loc.t -> Names.module_path -> string -> unit
+val dump_reference  : Loc.t -> string -> string -> string -> unit
+val dump_libref : Loc.t -> Names.dir_path -> string -> unit
 val dump_notation_location : (int * int) list -> Constrexpr.notation ->
   (Notation.notation_location * Notation_term.scope_name option) -> unit
-val dump_binding : Pp.loc -> Names.Idset.elt -> unit
+val dump_binding : Loc.t -> Names.Idset.elt -> unit
 val dump_notation :
-  Pp.loc * (Constrexpr.notation * Notation.notation_location) ->
+  Loc.t * (Constrexpr.notation * Notation.notation_location) ->
   Notation_term.scope_name option -> bool -> unit
 val dump_constraint :
   Constrexpr.typeclass_constraint -> bool -> string -> unit