From 1ca19082cf506c304b3c7945e72c0238f2aa9d1a Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 26 Jul 2016 14:22:42 +0200 Subject: restore compatibility with gallium's camlp4 (broken by commit 8e07227c) Apparently, in camlp4 (unlike camlp5) : - Something like "[ kwd = IDENT "foobar" -> .... kwd ... ]" produces a kwd of type token instead of string (which sounds reasonable ?). For now, I've replaced kwd by the explicit strings. Not so nice, but works with both camlp4 and camlp5 - A quotation of the form "let obj = ... in bar; baz" is not interpreted in the usual OCaml way, but rather as "(let obj = ... in bar); baz". Let's use instead "let obj = ... in let () = bar in baz", which works fine. --- grammar/tacextend.mlp | 4 ++-- parsing/g_vernac.ml4 | 10 +++++----- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index 2ec6430fd..a1b3f4f25 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -111,8 +111,8 @@ let declare_tactic loc s c cl = match cl with declare_str_items loc [ <:str_item< do { let obj () = Tacenv.register_ltac True False $name$ $body$ in - Tacenv.register_ml_tactic $se$ [|$tac$|]; - Mltop.declare_cache_obj obj $plugin_name$; } >> + let () = Tacenv.register_ml_tactic $se$ [|$tac$|] in + Mltop.declare_cache_obj obj $plugin_name$ } >> ] | _ -> (** Otherwise we add parsing and printing rules to generate a call to a diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index a4bceeb67..c09693b36 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -211,11 +211,11 @@ GEXTEND Gram | IDENT "Conjecture" -> (None, Conjectural) ] ] ; assumptions_token: - [ [ kwd = IDENT "Hypotheses" -> (kwd, (Some Discharge, Logical)) - | kwd = IDENT "Variables" -> (kwd, (Some Discharge, Definitional)) - | kwd = IDENT "Axioms" -> (kwd, (None, Logical)) - | kwd = IDENT "Parameters" -> (kwd, (None, Definitional)) - | kwd = IDENT "Conjectures" -> (kwd, (None, Conjectural)) ] ] + [ [ IDENT "Hypotheses" -> ("Hypotheses", (Some Discharge, Logical)) + | IDENT "Variables" -> ("Variables", (Some Discharge, Definitional)) + | IDENT "Axioms" -> ("Axioms", (None, Logical)) + | IDENT "Parameters" -> ("Parameters", (None, Definitional)) + | IDENT "Conjectures" -> ("Conjectures", (None, Conjectural)) ] ] ; inline: [ [ IDENT "Inline"; "("; i = INT; ")" -> InlineAt (int_of_string i) -- cgit v1.2.3