aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/lexer.mll
diff options
context:
space:
mode:
authorGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-04-28 16:00:15 +0000
committerGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-04-28 16:00:15 +0000
commitbd182166d8a97de81b6abdb3aa434cc32d95a9dc (patch)
treebaf2d5ef0691eaffeba3228f89877c8eef103411 /parsing/lexer.mll
parent897cb12c7d539e63d52a701bad92376acdf6a473 (diff)
portage en ocaml / camlp4 3.00
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@379 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/lexer.mll')
-rw-r--r--parsing/lexer.mll9
1 files changed, 6 insertions, 3 deletions
diff --git a/parsing/lexer.mll b/parsing/lexer.mll
index 6a35d19de..0f7b4938c 100644
--- a/parsing/lexer.mll
+++ b/parsing/lexer.mll
@@ -261,9 +261,12 @@ let token_text = function
| (con, prm) -> con ^ " \"" ^ prm ^ "\""
let tparse (p_con, p_prm) =
- if p_prm = "" then
- parser [< '(con, prm) when con = p_con >] -> prm
+ ifdef CAMLP4_300 then
+ None
else
- parser [< '(con, prm) when con = p_con && prm = p_prm >] -> prm
+ if p_prm = "" then
+ parser [< '(con, prm) when con = p_con >] -> prm
+ else
+ parser [< '(con, prm) when con = p_con && prm = p_prm >] -> prm
}