From 29bb2f7d9fecf06e3246142e649db4db0320da41 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 31 Aug 2014 01:55:32 +0200 Subject: Moving code of tactic interpretation from Tacenv to Vernacentries. This allows to directly register globtactics in the Tacenv API, without having to resort to any internalization function. --- grammar/tacextend.ml4 | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'grammar') 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$; } -- cgit v1.2.3