Generalized the formulation of classic_set in propositional contexts

(consequence of classical unique choice)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13030 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 11 insertions, 2 deletions

diff --git a/theories/Logic/ClassicalUniqueChoice.v b/theories/Logic/ClassicalUniqueChoice.v
index 67b853be9..6389e447f 100644
--- a/theories/Logic/ClassicalUniqueChoice.v
+++ b/theories/Logic/ClassicalUniqueChoice.v
@@ -46,9 +46,10 @@ Qed.
 
 Require Import Setoid.
 
-Theorem classic_set : ((forall P:Prop, {P} + {~ P}) -> False) -> False.
+Theorem classic_set_in_prop_context :
+  forall C:Prop, ((forall P:Prop, {P} + {~ P}) -> C) -> C.
 Proof.
-intro HnotEM.
+intros C HnotEM.
 set (R := fun A b => A /\ true = b \/ ~ A /\ false = b).
 assert (H :  exists f : Prop -> bool, (forall A:Prop, R A (f A))).
 apply unique_choice.
@@ -80,3 +81,11 @@ destruct (f P).
     assumption.
 Qed.
 
+Corollary not_not_classic_set :
+  ((forall P:Prop, {P} + {~ P}) -> False) -> False.
+Proof.
+apply classic_set_in_prop_context.
+Qed.
+
+(* Compatibility *)
+Notation classic_set := not_not_classic_set (only parsing).