aboutsummaryrefslogtreecommitdiff
path: root/parsing/pcoq.ml4
diff options
context:
space:
mode:
authorletouzey2007-09-15 10:35:59 +0000
committerletouzey2007-09-15 10:35:59 +0000
commitda3edaa7eab2bed17cdfb2c455f2e6b5b0318c4d (patch)
tree14b6ae25300dc08c9ca5ff86ad88a78910df7b92 /parsing/pcoq.ml4
parent4f39e160d05b0e5501a909b3041589303651670b (diff)
* 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
Diffstat (limited to 'parsing/pcoq.ml4')
-rw-r--r--parsing/pcoq.ml429
1 files changed, 27 insertions, 2 deletions
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 []