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, 7 insertions, 8 deletions

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 748e5297b..3553373fb 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -9,13 +9,12 @@
 open Pp
 open Names
 
-let pr_located = Loc.pr_located
-
-open Compat
+(* open Compat *)
 open Errors
 open Util
 open Extend
 open Vernacexpr
+open Pputils
 open Ppconstr
 open Pptactic
 open Libnames
@@ -28,8 +27,8 @@ let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr
 
 let pr_lident (loc,id) =
   if loc <> Loc.ghost then
-    let (b,_) = unloc loc in
-    pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id)
+    let (b,_) = Loc.unloc loc in
+    pr_located pr_id (Loc.make_loc (b,b+String.length(string_of_id id)),id)
   else pr_id id
 
 let string_of_fqid fqid =
@@ -39,8 +38,8 @@ let pr_fqid fqid = str (string_of_fqid fqid)
 
 let pr_lfqid (loc,fqid) =
   if loc <> Loc.ghost then
-   let (b,_) = unloc loc in
-    pr_located pr_fqid (make_loc (b,b+String.length(string_of_fqid fqid)),fqid)
+   let (b,_) = Loc.unloc loc in
+    pr_located pr_fqid (Loc.make_loc (b,b+String.length(string_of_fqid fqid)),fqid)
   else
    pr_fqid fqid
 
@@ -319,7 +318,7 @@ let pr_onescheme (idop,schem) =
 
 let begin_of_inductive = function
     [] -> 0
-  | (_,((loc,_),_))::_ -> fst (unloc loc)
+  | (_,((loc,_),_))::_ -> fst (Loc.unloc loc)
 
 let pr_class_rawexpr = function
   | FunClass -> str"Funclass"