blob: b2f00ffc659a80e6ca4ff30d54f66e1dc4f4db35 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
Parameter x y : nat.
Axiom H : x = y.
Hint Rewrite H : mybase.
Ltac bar base := autorewrite with base.
Tactic Notation "foo" ident(base) := autorewrite with base.
Goal x = 0.
bar mybase.
now_show (y = 0).
Undo 2.
foo mybase.
now_show (y = 0).
Abort.
|
