diff options
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/tacextend.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 312f0e949..dd00bc19a 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -201,10 +201,10 @@ let declare_tactic loc s c cl = match cl with the ML tactic retrieves its arguments in the [ist] environment instead. This is the rôle of the [lift_constr_tac_to_ml_tac] function. *) let body = <:expr< Tacexpr.TacFun ($vars$, Tacexpr.TacML ($dloc$, $se$, [])) >> in - let name = <:expr< Libnames.Ident($dloc$, Names.Id.of_string $name$) >> in + let name = <:expr< Names.Id.of_string $name$ >> in declare_str_items loc [ <:str_item< do { - let obj () = Tacenv.register_ltac False False [($name$, False, $body$)] in + let obj () = Tacenv.register_ltac False $name$ $body$ in try do { Tacenv.register_ml_tactic $se$ $tac$; Mltop.declare_cache_obj obj $plugin_name$; } |