aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/auto.v
blob: db3b19af517629addcae5c35eaa93fb40d8ee767 (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 occuring
   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.