diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-07-26 14:22:42 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-07-26 14:40:23 +0200 |
| commit | 1ca19082cf506c304b3c7945e72c0238f2aa9d1a (patch) | |
| tree | 8a5310fa205569d8eafbfa6d0be71b0f2b3b2472 /grammar | |
| parent | 273b8725e28e109b33f044079a36515d42068a8d (diff) | |
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.
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/tacextend.mlp | 4 |
1 files changed, 2 insertions, 2 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 |