max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init/meta/interactive): allow metavariable in change tactic

Browse source
This commit is contained in:
Jeremy Avigad 2016-12-09 15:52:09 -05:00 • committed by Leonardo de Moura
parent 55401a95ec
commit 1ba55e5cda
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/meta/interactive.lean
View file

@ -107,7 +107,7 @@ meta def assumption : tactic unit :=
tactic.assumption
meta def change (q : qexpr0) : tactic unit :=
to_expr_strict q >>= tactic.change
to_expr q >>= tactic.change
meta def exact (q : qexpr0) : tactic unit :=
do tgt : expr ← target,