1 files changed, 15 insertions, 0 deletions
diff --git a/test-suite/success/hintdb_in_ltac_bis.v b/test-suite/success/hintdb_in_ltac_bis.v
new file mode 100644
index 00000000..2bc3f9d2
--- /dev/null
+++ b/test-suite/success/hintdb_in_ltac_bis.v
@@ -0,0 +1,15 @@
+Parameter Foo : Prop.
+Axiom H : Foo.
+
+Hint Resolve H : mybase.
+
+Ltac foo base := eauto with base.
+
+Tactic Notation "bar" ident(base) :=
+  typeclasses eauto with base.
+
+Goal Foo.
+  progress foo mybase.
+  Undo.
+  progress bar mybase.
+Qed.