1
(* Submitted by Robert Schneck *)
3
Parameter A B C D : Prop.
4
Axiom X : A -> B -> C /\ D.
6
Lemma foo : A -> B -> C.
9
destruct X. (* Should find axiom X and should handle arguments of X *)
15
(* Simplification of bug 711 *)
17
Parameter f : true = false.
18
Goal let p := f in True.
21
(* Check that it doesn't fail with an anomaly *)
22
(* Ultimately, adapt destruct to make it succeeding *)
26
(* Used to fail with error "n is used in conclusion" before revision 9447 *)
28
Goal forall n, n = S n.
32
(* Check that elimination with remaining evars do not raise an bad
35
Theorem Refl : forall P, P <-> P. tauto. Qed.
37
case Refl || ecase Refl.
41
(* Submitted by B. Baydemir (bug #1882) *)
45
Definition alist R := list (nat * R)%type.
50
Variables E : alist A.
54
clear. induction E. (* this fails. *)