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

5 files changed, 40 insertions, 11 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 1d03716d0c..25ea991e7b 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -13,6 +13,7 @@ open Pp
 open Names
 open Nameops
 open Libnames
+open Pputils
 open Ppextend
 open Constrexpr
 open Constrexpr_ops
@@ -102,7 +103,7 @@ let pr_com_at n =
   if Flags.do_beautify() && n <> 0 then comment n
   else mt()
 
-let pr_with_comments loc pp = Loc.pr_located (fun x -> x) (loc,pp)
+let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp)
 
 let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c)
 
@@ -137,12 +138,12 @@ let pr_opt_type_spc pr = function
 let pr_lident (loc,id) =
   if loc <> Loc.ghost then
     let (b,_) = Loc.unloc loc in
-    Loc.pr_located pr_id (Loc.make_loc (b,b+String.length(string_of_id id)),id)
+    pr_located pr_id (Loc.make_loc (b,b+String.length(string_of_id id)),id)
   else pr_id id
 
 let pr_lname = function
     (loc,Name id) -> pr_lident (loc,id)
-  | lna -> Loc.pr_located pr_name lna
+  | lna -> pr_located pr_name lna
 
 let pr_or_var pr = function
   | ArgArg x -> pr x
diff --git a/printing/pputils.ml b/printing/pputils.ml
new file mode 100644
index 0000000000..0c54c61818
--- /dev/null
+++ b/printing/pputils.ml
@@ -0,0 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+
+let pr_located pr (loc, x) =
+  if Flags.do_beautify () && loc <> Loc.ghost then
+    let (b, e) = Loc.unloc loc in
+    Pp.comment b ++ pr x ++ Pp.comment e
+  else pr x
diff --git a/printing/pputils.mli b/printing/pputils.mli
new file mode 100644
index 0000000000..bac2815faf
--- /dev/null
+++ b/printing/pputils.mli
@@ -0,0 +1,13 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+
+val pr_located : ('a -> std_ppcmds) -> 'a Loc.located -> std_ppcmds
+(** Prints an object surrounded by its commented location *)
+
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 748e5297b2..3553373fb7 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"
diff --git a/printing/printing.mllib b/printing/printing.mllib
index 2de798aa45..6d6e1bba67 100644
--- a/printing/printing.mllib
+++ b/printing/printing.mllib
@@ -1,3 +1,4 @@
+Pputils
 Ppconstr
 Printer
 Pptactic