blob: bce7c3f23b1955f1b4b8a8c03393e4cc896792bf (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
Module JGross.
Hint Extern 1 => match goal with |- match ?E with end => case E end.
Goal forall H : False, match H return Set with end.
Proof.
intros.
Fail solve [ eauto ]. (* No applicable tactic *)
admit.
Qed.
End JGross.
Section BenDelaware.
Hint Extern 0 => admit.
Goal forall (H : False), id (match H return Set with end).
Proof.
eauto.
Qed.
Goal forall (H : False), match H return Set with end.
Proof.
Fail solve [ eauto ] .
admit.
Qed.
End BenDelaware.
|
