blob: 3bbb664f4f7da4bec244e9ced6a5f0fd1a2c0736 (
plain)
1
2
3
4
5
|
Theorem test (A:Prop) : A \/ A -> A.
Fail let H := idtac in intros H; destruct H as H'.
(* Disjunctive/conjunctive introduction pattern expected. *)
Fail let H' := idtac in intros H; destruct H as H'.
Abort.
|