blob: f07ee1e6cf9785a8b9ef57b6138c1f5e8ae0e5fd (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
Require Import TestSuite.admit.
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.
|
