blob: aaa7b3a514dbbd4db42d6a0386ba22d313e8784c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
|
(* Wish #2154 by E. van der Weegen *)
(* auto was not using f_equal-style lemmas with metavariables occurring
only in the type of an evar of the concl, but not directly in the
concl itself *)
Parameters
(F: Prop -> Prop)
(G: forall T, (T -> Prop) -> Type)
(L: forall A (P: A -> Prop), G A P -> forall x, F (P x))
(Q: unit -> Prop).
Hint Resolve L.
Goal G unit Q -> F (Q tt).
intro.
eauto.
Qed.
(* Test implicit arguments in "using" clause *)
Goal forall n:nat, nat * nat.
auto using (pair O).
Undo.
eauto using (pair O).
Qed.
Create HintDb test discriminated.
Parameter foo : forall x, x = x + 0.
Hint Resolve foo : test.
Variable C : nat -> Type -> Prop.
Variable c_inst : C 0 nat.
Hint Resolve c_inst : test.
Hint Mode C - + : test.
Hint Resolve c_inst : test2.
Hint Mode C + + : test2.
Goal exists n, C n nat.
Proof.
eexists. Fail progress debug eauto with test2.
progress eauto with test.
Qed.
|
