Add (almost) compatibility with camlp4, without breaking support for camlp5

The choice between camlp4/5 is done during configure with flags
 -usecamlp5 (default for the moment) vs. -usecamlp4.

 Currently, to have a full camlp4 compatibility, you need to change
 all "EXTEND" and "GEXTEND Gram" into "EXTEND Gram", and change "EOI"
 into "`EOI" in grammar entries. I've a sed script that does that
 (actually the converse), but I prefer to re-think it and check a few
 things before branching this sed into the build mechanism.

 lib/compat.ml4 is heavily used to hide incompatibilities between camlp4/5
 and try to propose a common interface (cf LexerSig / GrammarSig).
 A few incompatible quotations have been turned into underlying code
 manually, in order to make the IFDEF CAMLP5 THEN ... ELSE ... END
 parsable by both camlp4 and 5. See in particular the fate of
 <:str_item< declare ... end >>

 Stdpp isn't used anymore, but rather Ploc (hidden behind local module Loc).
 This forces to use camlp5 > 5.01.

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

6 files changed, 18 insertions, 14 deletions

diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 1b91ef1776..aebe1fca45 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -17,6 +17,7 @@ open Pretyping.Default
 open Rawterm
 open Term
 open Pp
+open Compat
 
 (* INTERN *)
 
@@ -85,10 +86,10 @@ let intern_fundecl args body globs=
 let rec add_vars_of_simple_pattern globs = function
     CPatAlias (loc,p,id) ->
       add_vars_of_simple_pattern (add_var id globs) p
-(*      Stdpp.raise_with_loc loc
+(*      Loc.raise loc
 	(UserError ("simple_pattern",str "\"as\" is not allowed here"))*)
   | CPatOr (loc, _)->
-      Stdpp.raise_with_loc loc
+      Loc.raise loc
 	(UserError ("simple_pattern",str "\"(_ | _)\" is not allowed here"))
   | CPatDelimiters (_,_,p) ->
       add_vars_of_simple_pattern globs p
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 28aa939750..11862747a3 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -11,7 +11,7 @@
 (* arnaud: veiller à l'aspect tutorial des commentaires *)
 
 open Pp
-
+open Tok
 open Decl_expr
 open Names
 open Term
@@ -85,9 +85,9 @@ let vernac_proof_instr instr =
 
 (* We create a new parser entry [proof_mode]. The Declarative proof mode
     will replace the normal parser entry for tactics with this one. *)
-let proof_mode = Gram.Entry.create "vernac:proof_command" 
+let proof_mode = Gram.entry_create "vernac:proof_command"
 (* Auxiliary grammar entry. *)
-let proof_instr = Gram.Entry.create "proofmode:instr"
+let proof_instr = Gram.entry_create "proofmode:instr"
 
 (* Before we can write an new toplevel command (see below) 
     which takes a [proof_instr] as argument, we need to declare
diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4
index 9e415b635c..e186dd76dc 100644
--- a/plugins/subtac/g_subtac.ml4
+++ b/plugins/subtac/g_subtac.ml4
@@ -33,11 +33,11 @@ module Tactic = Pcoq.Tactic
 
 module SubtacGram =
 struct
-  let gec s = Gram.Entry.create ("Subtac."^s)
+  let gec s = Gram.entry_create ("Subtac."^s)
 		(* types *)
-  let subtac_gallina_loc : Vernacexpr.vernac_expr located Gram.Entry.e = gec "subtac_gallina_loc"
+  let subtac_gallina_loc : Vernacexpr.vernac_expr located Gram.entry = gec "subtac_gallina_loc"
 
-  let subtac_withtac : Tacexpr.raw_tactic_expr option Gram.Entry.e = gec "subtac_withtac"
+  let subtac_withtac : Tacexpr.raw_tactic_expr option Gram.entry = gec "subtac_withtac"
 end
 
 open Rawterm
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 569aba2637..9214e451f4 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Compat
 open Global
 open Pp
 open Util
@@ -228,8 +229,8 @@ let subtac (loc, command) =
       debug 2 (Himsg.explain_pretype_error env exn);
       raise e
 
-  | (Stdpp.Exc_located (loc, Proof_type.LtacLocated (_,e')) |
-     Stdpp.Exc_located (loc, e') as e) ->
+  | (Loc.Exc_located (loc, Proof_type.LtacLocated (_,e')) |
+     Loc.Exc_located (loc, e') as e) ->
       debug 2 (str "Parsing exception: ");
       (match e' with
       | Type_errors.TypeError (env, exn) ->
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index c7d0eb67fb..591e01c04e 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -15,6 +15,7 @@ open Util
 open Evd
 open Declare
 open Proof_type
+open Compat
 
 let ppwarn cmd = Pp.warn (str"Program:" ++ cmd)
 let pperror cmd = Util.errorlabstrm "Program" cmd
@@ -484,8 +485,8 @@ and solve_obligation_by_tac prg obls i tac =
 	      true
 	  else false
 	with
-	| Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
-	| Stdpp.Exc_located(_, Refiner.FailError (_, s))
+	| Loc.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
+	| Loc.Exc_located(_, Refiner.FailError (_, s))
 	| Refiner.FailError (_, s) ->
 	    user_err_loc (obl.obl_location, "solve_obligation", Lazy.force s)
 	| Util.Anomaly _ as e -> raise e
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 0dda9b9e88..87c67cc147 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Compat
 open Util
 open Names
 open Sign
@@ -270,7 +271,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	      make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
 	  | RCoFix i ->
 	      let cofix = (i,(names,ftys,fdefs)) in
-	      (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e);
+	      (try check_cofix env cofix with e -> Loc.raise loc e);
 	      make_judge (mkCoFix cofix) ftys.(i) in
 	inh_conv_coerce_to_tycon loc env evdref fixj tycon
 
@@ -357,7 +358,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	let j' = pretype_type empty_valcon env' evdref lvar c2 in
 	let resj =
 	  try judge_of_product env name j j'
-	  with TypeError _ as e -> Stdpp.raise_with_loc loc e in
+	  with TypeError _ as e -> Loc.raise loc e in
 	  inh_conv_coerce_to_tycon loc env evdref resj tycon
 
     | RLetIn(loc,name,c1,c2)      ->