blob: f12b4d1f4516bb6662ae2d9832502e2c28921922 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
Definition x := 0.
Hint Unfold x : mybase.
Ltac autounfoldify base := autounfold with base.
Tactic Notation "autounfoldify_bis" ident(base) := autounfold with base.
Goal x = 0.
progress autounfoldify mybase.
Undo.
progress autounfoldify_bis mybase.
trivial.
Qed.
|
