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

4 files changed, 16 insertions, 13 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 4b565ddbd9..1a30b4e2cf 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Compat
 open Util
 open Names
 open Nameops
@@ -42,7 +43,7 @@ type pattern_matching_error =
 exception PatternMatchingError of env * pattern_matching_error
 
 let raise_pattern_matching_error (loc,ctx,te) =
-  Stdpp.raise_with_loc loc (PatternMatchingError(ctx,te))
+  Loc.raise loc (PatternMatchingError(ctx,te))
 
 let error_bad_pattern_loc loc cstr ind =
   raise_pattern_matching_error (loc, Global.env(), BadPattern (cstr,ind))
@@ -98,7 +99,7 @@ let rec list_try_compile f = function
   | h::t ->
       try f h
       with UserError _ | TypeError _ | PretypeError _
-	| Stdpp.Exc_located (_,(UserError _ | TypeError _ | PretypeError _)) ->
+	| Loc.Exc_located (_,(UserError _ | TypeError _ | PretypeError _)) ->
 	    list_try_compile f t
 
 let force_name =
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 6adaee81c2..5b829e5bf4 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -6,8 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Compat
 open Util
-open Stdpp
 open Names
 open Sign
 open Term
@@ -41,7 +41,7 @@ exception PretypeError of env * pretype_error
 
 let precatchable_exception = function
   | Util.UserError _ | TypeError _ | PretypeError _
-  | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ |
+  | Loc.Exc_located(_,(Util.UserError _ | TypeError _ |
     Nametab.GlobalizationError _ | PretypeError _)) -> true
   | _ -> false
 
@@ -96,10 +96,10 @@ let contract3 env a b c = match contract env [a;b;c] with
   | env, [a;b;c] -> env,a,b,c | _ -> assert false
 
 let raise_pretype_error (loc,ctx,sigma,te) =
-  Stdpp.raise_with_loc loc (PretypeError(env_ise sigma ctx,te))
+  Loc.raise loc (PretypeError(env_ise sigma ctx,te))
 
 let raise_located_type_error (loc,ctx,sigma,te) =
-  Stdpp.raise_with_loc loc (TypeError(env_ise sigma ctx,te))
+  Loc.raise loc (TypeError(env_ise sigma ctx,te))
 
 
 let error_actual_type_loc loc env sigma {uj_val=c;uj_type=actty} expty =
@@ -155,11 +155,11 @@ let error_occur_check env sigma ev c =
 
 let error_not_clean env sigma ev c (loc,k) =
   let c = nf_evar sigma c in
-  raise_with_loc loc
+  Loc.raise loc
     (PretypeError (env_ise sigma env,  NotClean (ev,c,k)))
 
 let error_unsolvable_implicit loc env sigma evi e explain =
-  raise_with_loc loc
+  Loc.raise loc
     (PretypeError (env_ise sigma env, UnsolvableImplicit (evi, e, explain)))
 
 let error_cannot_unify env sigma (m,n) =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 70241238db..22a3451c4b 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -21,6 +21,7 @@
 (* Secondary maintenance: collective *)
 
 
+open Compat
 open Pp
 open Util
 open Names
@@ -66,7 +67,7 @@ let search_guard loc env possible_indexes fixdefs =
     let indexes = Array.of_list (List.map List.hd possible_indexes) in
     let fix = ((indexes, 0),fixdefs) in
     (try check_fix env fix with
-       | e -> if loc = dummy_loc then raise e else Stdpp.raise_with_loc loc e);
+       | e -> if loc = dummy_loc then raise e else Loc.raise loc e);
     indexes
   else
     (* we now search recursively amoungst all combinations *)
@@ -396,7 +397,7 @@ module Pretyping_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
 
@@ -464,7 +465,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	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)      ->
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 869a7845d1..983942abad 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -16,6 +16,7 @@ open Environ
 open Nametab
 open Mod_subst
 open Topconstr
+open Compat
 open Util
 open Libnames
 (*i*)
@@ -45,7 +46,7 @@ let unsatisfiable_constraints env evd ev =
       raise (TypeClassError (env, UnsatisfiableConstraints (evd, None)))
   | Some ev ->
       let loc, kind = Evd.evar_source ev evd in
-	raise (Stdpp.Exc_located (loc, TypeClassError
+	raise (Loc.Exc_located (loc, TypeClassError
 	  (env, UnsatisfiableConstraints (evd, Some (ev, kind)))))
 
 let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m))
@@ -53,5 +54,5 @@ let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstan
 let rec unsatisfiable_exception exn =
   match exn with
   | TypeClassError (_, UnsatisfiableConstraints _) -> true
-  | Stdpp.Exc_located(_, e) -> unsatisfiable_exception e
+  | Loc.Exc_located(_, e) -> unsatisfiable_exception e
   | _ -> false