* Adding compability with ocaml 3.10 + camlp5 (rework of

  the patch by S. Mimram)
* for detecting architecture, also look for /bin/uname
* restore the compatibility of kernel/byterun/coq_interp.c with 
  ocaml 3.07 (caml_modify vs. modify). There is still an issue 
  with this 3.07 and 64-bits architecture (see coqdev and a future 
  bug report). 




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

5 files changed, 44 insertions, 14 deletions

diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 7585ad4d86..b4fa39bebe 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -14,7 +14,7 @@ open Genarg
 open Q_util
 open Q_coqast
 
-let join_loc (deb1,_) (_,fin2) = (deb1,fin2)
+let join_loc = Util.join_loc
 let loc = Util.dummy_loc
 let default_loc = <:expr< Util.dummy_loc >>
 
@@ -228,7 +228,7 @@ EXTEND
         let t, g = interp_entry_name loc e sep in (g, Some (s,t))
       | s = STRING ->
 	  if String.length s > 0 && Util.is_letter s.[0] then
-	    Pcoq.lexer.Token.using ("", s);
+	    Compat.using Pcoq.lexer ("", s);
         (<:expr< (Gramext.Stoken (Lexer.terminal $str:s$)) >>, None)
     ] ]
   ;
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index 8de2af4ec6..e99741a6e0 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -45,7 +45,7 @@ val extend_grammar : all_grammar_command -> unit
 type grammar_tactic_production =
   | TacTerm of string
   | TacNonTerm of
-      loc * (Token.t Gramext.g_symbol * Genarg.argument_type) * string option
+      loc * (Compat.token Gramext.g_symbol * Genarg.argument_type) * string option
 
 val extend_tactic_grammar :
   string -> grammar_tactic_production list list -> unit
@@ -61,7 +61,7 @@ val get_extend_vernac_grammars :
 (*
 val reset_extend_grammars_v8 : unit -> unit
 *)
-val interp_entry_name : int -> string -> entry_type * Token.t Gramext.g_symbol
+val interp_entry_name : int -> string -> entry_type * Compat.token Gramext.g_symbol
 
 val recover_notation_grammar :
   notation -> (precedence * tolerability list) -> notation_grammar
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 161a08bfa7..b0e573eb91 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4use: "pa_extend.cmo" i*)
+(*i camlp4use: "pa_extend.cmo pa_macro.cmo" i*)
 
 (*i $Id$ i*)
 
@@ -31,6 +31,29 @@ open Ppextend
    we unfreeze the state of the lexer. This restores the behaviour of the
    lexer. B.B. *)
 
+IFDEF CAMLP5 THEN 
+
+let lexer = {
+  Token.tok_func = Lexer.func;
+  Token.tok_using = Lexer.add_token;
+  Token.tok_removing = (fun _ -> ());
+  Token.tok_match = Token.default_match;
+  (* Token.parse = Lexer.tparse; *)
+  Token.tok_comm = None;
+  Token.tok_text = Lexer.token_text }
+
+module L =
+  struct
+    type te = string * string
+    let lexer = lexer
+  end
+
+(* The parser of Coq *)
+
+module G = Grammar.GMake(L)
+
+ELSE 
+
 let lexer = {
   Token.func = Lexer.func;
   Token.using = Lexer.add_token;
@@ -47,6 +70,8 @@ module L =
 
 module G = Grammar.Make(L)
 
+END
+
 let grammar_delete e pos rls =
   List.iter
     (fun (n,ass,lev) ->
@@ -106,7 +131,7 @@ type ext_kind =
   | ByGrammar of
       grammar_object G.Entry.e * Gramext.position option *
       (string option * Gramext.g_assoc option *
-       (Token.t Gramext.g_symbol list * Gramext.g_action) list) list
+       (Compat.token Gramext.g_symbol list * Gramext.g_action) list) list
   | ByGEXTEND of (unit -> unit) * (unit -> unit)
 
 let camlp4_state = ref []
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 523ad92fb4..f0d10dcb0a 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -20,9 +20,9 @@ open Libnames
 
 (* The lexer and parser of Coq. *)
 
-val lexer : Token.lexer
+val lexer : Compat.lexer
 
-module Gram : Grammar.S with type te = Token.t
+module Gram : Grammar.S with type te = Compat.token
 
 (* The superclass of all grammar entries *)
 type grammar_object
@@ -42,7 +42,7 @@ val get_constr_entry :
 val grammar_extend :
   grammar_object Gram.Entry.e -> Gramext.position option ->
     (string option * Gramext.g_assoc option *
-     (Token.t Gramext.g_symbol list * Gramext.g_action) list) list
+     (Compat.token Gramext.g_symbol list * Gramext.g_action) list) list
     -> unit
 
 val remove_grammars : int -> unit
@@ -210,7 +210,7 @@ module Vernac_ :
 (* Binding entry names to campl4 entries *)
 
 val symbol_of_production : Gramext.g_assoc option -> constr_entry ->
-  bool -> constr_production_entry -> Token.t Gramext.g_symbol
+  bool -> constr_production_entry -> Compat.token Gramext.g_symbol
 
 (* Registering/resetting the level of an entry *)
 
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index f5bab5d69d..4b1dfd9e36 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4use: "q_MLast.cmo pa_ifdef.cmo" i*)
+(*i camlp4use: "q_MLast.cmo pa_macro.cmo" i*)
 
 (* $Id$ *)
 
@@ -21,13 +21,18 @@ let purge_str s =
   if String.length s == 0 || s.[0] <> '$' then s
   else String.sub s 1 (String.length s - 1)
 
+IFDEF OCAML308 THEN DEFINE NOP END
+IFDEF OCAML309 THEN DEFINE NOP END
+IFDEF CAMLP5 THEN DEFINE NOP END
+
 let anti loc x =
   let e =
     let loc =
-      ifdef OCAML_308 then
+      IFDEF NOP THEN 
         loc
-      else
-        (1, snd loc - fst loc)
+      ELSE 
+	(1, snd loc - fst loc)
+      END 
     in <:expr< $lid:purge_str x$ >>
   in
   <:expr< $anti:e$ >>