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

3 files changed, 6 insertions, 4 deletions

diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index e8e81c472c..a3052320cf 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -10,6 +10,7 @@
 
 (* arnaud: veiller à l'aspect tutorial des commentaires *)
 
+open Compat
 open Pp
 open Tok
 open Decl_expr
@@ -189,7 +190,7 @@ GLOBAL: proof_instr;
   statement :
     [[ i=ident ; ":" ; c=constr -> {st_label=Name i;st_it=c}
      | i=ident -> {st_label=Anonymous;
-		   st_it=Constrexpr.CRef (Libnames.Ident (loc, i))}
+		   st_it=Constrexpr.CRef (Libnames.Ident (!@loc, i))}
      | c=constr -> {st_label=Anonymous;st_it=c}
      ]];
   constr_or_thesis :
@@ -202,7 +203,7 @@ GLOBAL: proof_instr;
     |
       [ i=ident ; ":" ; cot=constr_or_thesis -> {st_label=Name i;st_it=cot}
       | i=ident -> {st_label=Anonymous;
-		    st_it=This (Constrexpr.CRef (Libnames.Ident (loc, i)))}
+		    st_it=This (Constrexpr.CRef (Libnames.Ident (!@loc, i)))}
       | c=constr -> {st_label=Anonymous;st_it=This c}
       ]
     ];
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 3039324847..160ca1b4c0 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -104,7 +104,7 @@ open Genarg
 open Ppconstr
 open Printer
 let pr_firstorder_using_raw _ _ _ = prlist_with_sep pr_comma pr_reference
-let pr_firstorder_using_glob _ _ _ = prlist_with_sep pr_comma (pr_or_var (Loc.pr_located pr_global))
+let pr_firstorder_using_glob _ _ _ = prlist_with_sep pr_comma (pr_or_var (fun x -> (pr_global (snd x))))
 let pr_firstorder_using_typed _ _ _ = prlist_with_sep pr_comma pr_global
 
 ARGUMENT EXTEND firstorder_using
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 77c6dc4938..0dceecf4f1 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 (*i camlp4deps: "grammar/grammar.cma" i*)
+open Compat
 open Util
 open Term
 open Names
@@ -145,7 +146,7 @@ GEXTEND Gram
   GLOBAL: function_rec_definition_loc ;
 
   function_rec_definition_loc:
-    [ [ g = Vernac.rec_definition -> loc, g ]]
+    [ [ g = Vernac.rec_definition -> !@loc, g ]]
     ;
 
   END