blob: 9daf9647fce6eaee16773cc6804f94aae35de70d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
(* Checking that classical_right/classical_left work in an empty context *)
Require Import Classical.
Parameter A:Prop.
Goal A \/ ~A.
classical_right.
assumption.
Qed.
Goal ~A \/ A.
classical_left.
assumption.
Qed.
|