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 /configure.ml | |
| 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.
Diffstat (limited to 'configure.ml')
0 files changed, 0 insertions, 0 deletions