blob: 02f88b72700bbdd7f5c00eba7124c5ee25905f92 (
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
|
(* Submitted by Robert Schneck *)
Parameter A B C D : Prop.
Axiom X : A -> B -> C /\ D.
Lemma foo : A -> B -> C.
Proof.
intros.
destruct X. (* Should find axiom X and should handle arguments of X *)
assumption.
assumption.
assumption.
Qed.
(* Simplification of bug 711 *)
Parameter f : true = false.
Goal let p := f in True.
intro p.
set (b := true) in *.
(* Check that it doesn't fail with an anomaly *)
(* Ultimately, adapt destruct to make it succeeding *)
try destruct b.
Abort.
(* Used to fail with error "n is used in conclusion" before revision 9447 *)
Goal forall n, n = S n.
induction S.
Abort.
(* Check that elimination with remaining evars do not raise an bad
error message *)
Theorem Refl : forall P, P <-> P. tauto. Qed.
Goal True.
case Refl || ecase Refl.
Abort.
|
