diff options
Diffstat (limited to 'grammar/tacextend.ml4')
| -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 f11927e77..8b5b64ffc 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -177,7 +177,7 @@ let declare_tactic loc s cl = let e = make_fun <:expr< - Refiner.abstract_extended_tactic $mlexpr_of_string s$ $make_args p$ $make_eval_tactic e p$ + Refiner.abstract_extended_tactic $make_eval_tactic e p$ >> p in <:str_item< value $lid:stac$ = $e$ >> |