Moved Compat to parsing. This permits to break the dependency of the

kernel on CAMLP4/5 structures, and consequently should also erase
such structures from vo files.

This modification requires some code duplication, mainly while
reimplementing our own location data type. This is chiefly visible
in the ml4 files, where CAMLP4/5 locations must be manually converted
to our locations with an explicit (!@) cast operator.

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

1 files changed, 17 insertions, 4 deletions

diff --git a/lib/loc.mli b/lib/loc.mli
index c1cbdb64d..0b6ba544d 100644
--- a/lib/loc.mli
+++ b/lib/loc.mli
@@ -8,21 +8,37 @@
 
 (** {5 Basic types} *)
 
-type t = Compat.Loc.t
+type t
 
 exception Exc_located of t * exn
 
 type 'a located = t * 'a
+(** Embed a location in a type *)
 
 (** {5 Location manipulation} *)
 
 (** This is inherited from CAMPL4/5. *)
 
+val create : string -> int -> int -> (int * int) -> t
+(** Create a location from a filename, a line number, a position of the
+    beginning of the line and a pair of start and end position *)
+
 val unloc : t -> int * int
+(** Return the start and end position of a location *)
+
 val make_loc : int * int -> t
+(** Make a location out of its start and end position *)
+
 val ghost : t
+(** Dummy location *)
+
 val merge : t -> t -> t
+
 val raise : t -> exn -> 'a
+(** Raise a located exception *)
+
+val represent : t -> (string * int * int * int * int)
+(** Return the arguments given in [create] *)
 
 (** {5 Location utilities} *)
 
@@ -32,9 +48,6 @@ val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit
 val down_located : ('a -> 'b) -> 'a located -> 'b
 (** Projects out a located object *)
 
-val pr_located : ('a -> Pp.std_ppcmds) -> 'a located -> Pp.std_ppcmds
-(** Prints an object surrounded by its commented location *)
-
 (** {5 Backward compatibility} *)
 
 val dummy_loc : t