aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/hintdb_in_ltac.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/success/hintdb_in_ltac.v')
-rw-r--r--test-suite/success/hintdb_in_ltac.v14
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 000000000..f12b4d1f4
--- /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.