diff options
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/tacextend.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index aec115b7ef..25ce4cdafe 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -204,7 +204,7 @@ let declare_tactic loc s c cl = match cl with let name = <:expr< Names.Id.of_string $name$ >> in declare_str_items loc [ <:str_item< do { - let obj () = Tacenv.register_ltac False $name$ $body$ in + let obj () = Tacenv.register_ltac ~{for_ml=True} False $name$ $body$ in try do { Tacenv.register_ml_tactic $se$ $tac$; Mltop.declare_cache_obj obj $plugin_name$; } |