diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-06 15:10:27 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-06 15:42:27 +0100 |
| commit | d3653c6da5770dfc4d439639b49193e30172763a (patch) | |
| tree | b2f1e14b4406f11f595f1821353e77f167ff5336 | |
| parent | b18bc8d5fe64d395197b172b5574f03d50d8157d (diff) | |
Fixing bug #4610: Fails to build with camlp4 since the TACTIC EXTEND move.
We just reuse the same one weird old trick in CAMLP4 to compare keywords and
identifiers as tokens. Note though that the commit 982460743 does not fix the
keyword vs. identifier issue in CAMLP4, so that the corresponding test fails.
This means that since that commit, some code compiling with CAMLP5 does not
when using CAMLP4, making it a second-class citizen.
| -rw-r--r-- | dev/printers.mllib | 2 | ||||
| -rw-r--r-- | grammar/grammar.mllib | 2 | ||||
| -rw-r--r-- | parsing/compat.ml4 | 2 | ||||
| -rw-r--r-- | parsing/tok.mli | 1 |
4 files changed, 4 insertions, 3 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index 21868203f..39e4b1cdb 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -19,6 +19,7 @@ Pp_control Loc CList CString +Tok Compat Flags Control @@ -153,7 +154,6 @@ Library States Genprint -Tok Lexer Ppextend Pputils diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index 4432f4306..fc7cb392b 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -49,8 +49,8 @@ Stdarg Constrarg Constrexpr_ops -Compat Tok +Compat Lexer Entry Pcoq diff --git a/parsing/compat.ml4 b/parsing/compat.ml4 index 0e416fe32..c482c694e 100644 --- a/parsing/compat.ml4 +++ b/parsing/compat.ml4 @@ -276,7 +276,7 @@ ELSE module Gramext = G let stoken tok = match tok with | Tok.KEYWORD s -> Gramext.Skeyword s - | tok -> Gramext.Stoken ((=) tok, G.Token.to_string tok) + | tok -> Gramext.Stoken (Tok.equal tok, G.Token.to_string tok) END IFDEF CAMLP5_6_00 THEN diff --git a/parsing/tok.mli b/parsing/tok.mli index 416ce468e..54b747952 100644 --- a/parsing/tok.mli +++ b/parsing/tok.mli @@ -20,6 +20,7 @@ type t = | BULLET of string | EOI +val equal : t -> t -> bool val extract_string : t -> string val to_string : t -> string (* Needed to fit Camlp4 signature *) |