From ed9ab22b8c3b2210f479689f46d3e4b2fd4f52df Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sat, 17 Dec 2016 13:00:55 +0100
Subject: Add test-suite files for hintdb variables in Ltac.

In particular, this closes bug 2417.
---
 test-suite/bugs/closed/2417.v           | 15 +++++++++++++++
 test-suite/success/hintdb_in_ltac.v     | 14 ++++++++++++++
 test-suite/success/hintdb_in_ltac_bis.v | 15 +++++++++++++++
 3 files changed, 44 insertions(+)
 create mode 100644 test-suite/bugs/closed/2417.v
 create mode 100644 test-suite/success/hintdb_in_ltac.v
 create mode 100644 test-suite/success/hintdb_in_ltac_bis.v

diff --git a/test-suite/bugs/closed/2417.v b/test-suite/bugs/closed/2417.v
new file mode 100644
index 0000000000..b2f00ffc65
--- /dev/null
+++ b/test-suite/bugs/closed/2417.v
@@ -0,0 +1,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.
diff --git a/test-suite/success/hintdb_in_ltac.v b/test-suite/success/hintdb_in_ltac.v
new file mode 100644
index 0000000000..f12b4d1f45
--- /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.
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 0000000000..f5c25540ef
--- /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.
\ No newline at end of file
-- 
cgit v1.2.3