diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2016-12-17 13:00:55 +0100 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-02-07 17:38:00 +0100 |
| commit | ed9ab22b8c3b2210f479689f46d3e4b2fd4f52df (patch) | |
| tree | 8d82cd66f227abd83ce060dd8e27c93bfb2e43a8 /test-suite/success/hintdb_in_ltac_bis.v | |
| parent | 9e87e9582ffe68ff549347d4fab37f7514992361 (diff) | |
Add test-suite files for hintdb variables in Ltac.
In particular, this closes bug 2417.
Diffstat (limited to 'test-suite/success/hintdb_in_ltac_bis.v')
| -rw-r--r-- | test-suite/success/hintdb_in_ltac_bis.v | 15 |
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 000000000..f5c25540e --- /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 |