From d3653c6da5770dfc4d439639b49193e30172763a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 6 Mar 2016 15:10:27 +0100 Subject: 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. --- grammar/grammar.mllib | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'grammar') 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 -- cgit v1.2.3