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.