blob: 3a7de456701c5c911754ebe9eeae9fdca262cf24 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
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.
solve [ eauto ].
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.
solve [ eauto ] .
Qed.
End BenDelaware.
|
