aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/hintdb_in_ltac_bis.v
blob: 2bc3f9d22a929b986f209a690b05cc552b17f2b8 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
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.