diff options
| author | Pierre Letouzey | 2016-07-26 16:16:08 +0200 |
|---|---|---|
| committer | Pierre Letouzey | 2016-07-26 16:16:08 +0200 |
| commit | dc1db99e019242c07f00837f8316a8d392c40258 (patch) | |
| tree | ff271f3a63d9b4e7e6bf6bde4c590003c549c2c4 /grammar | |
| parent | 139204928e55f92f02d3b3dd1d6746e34fdcdb88 (diff) | |
| parent | 1ca19082cf506c304b3c7945e72c0238f2aa9d1a (diff) | |
Merge branch 'v8.6' into trunk
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 2ec6430fdd..a1b3f4f255 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 |