diff options
Diffstat (limited to 'test-suite/success/hintdb_in_ltac.v')
| -rw-r--r-- | test-suite/success/hintdb_in_ltac.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/test-suite/success/hintdb_in_ltac.v b/test-suite/success/hintdb_in_ltac.v new file mode 100644 index 00000000..f12b4d1f --- /dev/null +++ b/test-suite/success/hintdb_in_ltac.v @@ -0,0 +1,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. |