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, 27 insertions, 23 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 38ae4b9058..ba83fb5a80 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -35,6 +35,7 @@ open Pfedit
 open Command
 open Libnames
 open Evd
+open Compat
 
 let default_eauto_depth = 100
 let typeclasses_db = "typeclass_instances"
@@ -205,7 +206,7 @@ let e_possible_resolve db_list local_db gl =
 
 let rec catchable = function
   | Refiner.FailError _ -> true
-  | Stdpp.Exc_located (_, e) -> catchable e
+  | Loc.Exc_located (_, e) -> catchable e
   | e -> Logic.catchable_exception e
 
 let is_ground gl =
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 595917bdff..b51cb9d4be 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -15,7 +15,7 @@ open Evd
 open Environ
 open Explore
 
-val hintbases : hint_db_name list option Pcoq.Gram.Entry.e
+val hintbases : hint_db_name list option Pcoq.Gram.entry
 val wit_hintbases : hint_db_name list option typed_abstract_argument_type
 val rawwit_hintbases : hint_db_name list option raw_abstract_argument_type
 
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index ffa1bd747c..2c750be366 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -16,15 +16,15 @@ open Rawterm
 
 val rawwit_orient : bool raw_abstract_argument_type
 val wit_orient : bool typed_abstract_argument_type
-val orient : bool Pcoq.Gram.Entry.e
+val orient : bool Pcoq.Gram.entry
 
-val occurrences : (int list or_var) Pcoq.Gram.Entry.e
+val occurrences : (int list or_var) Pcoq.Gram.entry
 val rawwit_occurrences : (int list or_var) raw_abstract_argument_type
 val wit_occurrences : (int list) typed_abstract_argument_type
 
 val rawwit_raw : constr_expr raw_abstract_argument_type
 val wit_raw : (Tacinterp.interp_sign * rawconstr) typed_abstract_argument_type
-val raw : constr_expr Pcoq.Gram.Entry.e
+val raw : constr_expr Pcoq.Gram.entry
 
 type 'id gen_place= ('id * hyp_location_flag,unit) location
 
@@ -33,17 +33,17 @@ type place = identifier gen_place
 
 val rawwit_hloc : loc_place raw_abstract_argument_type
 val wit_hloc : place typed_abstract_argument_type
-val hloc : loc_place Pcoq.Gram.Entry.e
+val hloc : loc_place Pcoq.Gram.entry
 
 
-val in_arg_hyp:  (Names.identifier Util.located list option * bool)  Pcoq.Gram.Entry.e
+val in_arg_hyp:  (Names.identifier Util.located list option * bool)  Pcoq.Gram.entry
 val rawwit_in_arg_hyp : (Names.identifier Util.located list option * bool) raw_abstract_argument_type
 val wit_in_arg_hyp : (Names.identifier list option * bool) typed_abstract_argument_type
 val raw_in_arg_hyp_to_clause : (Names.identifier Util.located list option * bool) -> Tacticals.clause
 val glob_in_arg_hyp_to_clause :  (Names.identifier list option * bool)  -> Tacticals.clause
 
 
-val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.Entry.e
+val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.entry
 val rawwit_by_arg_tac :  raw_tactic_expr option raw_abstract_argument_type
 val wit_by_arg_tac : glob_tactic_expr option typed_abstract_argument_type
 
@@ -51,6 +51,6 @@ val wit_by_arg_tac : glob_tactic_expr option typed_abstract_argument_type
 
 (** Spiwack: Primitive for retroknowledge registration *)
 
-val retroknowledge_field : Retroknowledge.field Pcoq.Gram.Entry.e
+val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry
 val rawwit_retroknowledge_field :  Retroknowledge.field raw_abstract_argument_type
 val wit_retroknowledge_field : Retroknowledge.field typed_abstract_argument_type
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index d2381332ec..4827c77b63 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -36,6 +36,7 @@ open Pfedit
 open Command
 open Libnames
 open Evd
+open Compat
 
 (** Typeclass-based generalized rewriting. *)
 
@@ -1052,7 +1053,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl =
 	      else tclIDTAC
 	    in tclTHENLIST [evartac; rewtac] gl
 	  with
-	  | Stdpp.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e)))
+	  | Loc.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e)))
 	  | TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
 	      Refiner.tclFAIL_lazy 0
 		(lazy (str"setoid rewrite failed: unable to satisfy the rewriting constraints."
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 59d5cc3134..3d5f2ba1bb 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -46,6 +46,7 @@ open Pretyping
 open Pretyping.Default
 open Extrawit
 open Pcoq
+open Compat
 
 let safe_msgnl s =
     try msgnl s with e ->
@@ -90,15 +91,15 @@ let dloc = dummy_loc
 let catch_error call_trace tac g =
   if call_trace = [] then tac g else try tac g with
   | LtacLocated _ as e -> raise e
-  | Stdpp.Exc_located (_,LtacLocated _) as e -> raise e
+  | Loc.Exc_located (_,LtacLocated _) as e -> raise e
   | e ->
     let (nrep,loc',c),tail = list_sep_last call_trace in
-    let loc,e' = match e with Stdpp.Exc_located(loc,e) -> loc,e | _ ->dloc,e in
+    let loc,e' = match e with Loc.Exc_located(loc,e) -> loc,e | _ ->dloc,e in
     if tail = [] then
       let loc = if loc = dloc then loc' else loc in
-      raise (Stdpp.Exc_located(loc,e'))
+      raise (Loc.Exc_located(loc,e'))
     else
-      raise (Stdpp.Exc_located(loc',LtacLocated((nrep,c,tail,loc),e')))
+      raise (Loc.Exc_located(loc',LtacLocated((nrep,c,tail,loc),e')))
 
 (* Signature for interpretation: val_interp and interpretation functions *)
 type interp_sign =
@@ -1955,14 +1956,14 @@ and eval_with_fail ist is_lazy goal tac =
 	VRTactic (catch_error trace tac goal)
     | a -> a)
   with
-    | FailError (0,s) | Stdpp.Exc_located(_, FailError (0,s))
-    | Stdpp.Exc_located(_,LtacLocated (_,FailError (0,s))) ->
+    | FailError (0,s) | Loc.Exc_located(_, FailError (0,s))
+    | Loc.Exc_located(_,LtacLocated (_,FailError (0,s))) ->
 	raise (Eval_fail (Lazy.force s))
     | FailError (lvl,s) -> raise (FailError (lvl - 1, s))
-    | Stdpp.Exc_located(s,FailError (lvl,s')) ->
-	raise (Stdpp.Exc_located(s,FailError (lvl - 1, s')))
-    | Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) ->
-	raise (Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl - 1, s'))))
+    | Loc.Exc_located(s,FailError (lvl,s')) ->
+	raise (Loc.Exc_located(s,FailError (lvl - 1, s')))
+    | Loc.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) ->
+	raise (Loc.Exc_located(s,LtacLocated (s'',FailError (lvl - 1, s'))))
 
 (* Interprets the clauses of a recursive LetIn *)
 and interp_letrec ist gl llc u =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 21a9ee258e..5c96c138ea 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Compat
 open Pp
 open Util
 open Names
@@ -951,9 +952,9 @@ let general_apply with_delta with_destruct with_evars (loc,(c,lbind)) gl0 =
 	    with PretypeError _|RefinerError _|UserError _|Failure _|Exit ->
 	      if with_destruct then
                 descend_in_conjunctions
-                  try_main_apply (fun _ -> Stdpp.raise_with_loc loc exn) c gl
+                  try_main_apply (fun _ -> Loc.raise loc exn) c gl
 	      else
-		Stdpp.raise_with_loc loc exn
+		Loc.raise loc exn
 	in try_red_apply thm_ty0
   in
   try_main_apply with_destruct c gl0
@@ -1109,7 +1110,7 @@ let clear_wildcards ids =
     try with_check (Tacmach.thin_no_check [id]) gl
     with ClearDependencyError (id,err) ->
       (* Intercept standard [thin] error message *)
-      Stdpp.raise_with_loc loc
+      Loc.raise loc
         (error_clear_dependency (pf_env gl) (id_of_string "_") err))
     ids