test-suite/bugs/closed/5713.v


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.