From 9e95b47304c98e4bc41b6b31bf5ef96aba410851 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 2 Nov 2003 22:58:23 +0000
Subject: Renforcement significatif du resultat principal

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4779 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Logic/ClassicalDescription.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v
index 82077696d3..144d7d06a1 100644
--- a/theories/Logic/ClassicalDescription.v
+++ b/theories/Logic/ClassicalDescription.v
@@ -44,9 +44,9 @@ Qed.
 
 (** The followig proof comes from [1] *)
 
-Theorem classic_set : (P:Prop)({P}+{~P} -> False) -> False.
+Theorem classic_set : (((P:Prop){P}+{~P}) -> False) -> False.
 Proof.
-Intros P HnotEM.
+Intro HnotEM.
 Pose R:=[A,b]A/\true=b \/ ~A/\false=b.
 Assert H:(EX f:Prop->bool|(A:Prop)(R A (f A))).
 Apply description.
@@ -64,6 +64,7 @@ NewDestruct (classic A) as [Ha|Hnota].
       Assumption.
 NewDestruct H as [f Hf].
 Apply HnotEM.
+Intro P.
 Assert HfP := (Hf P).
 (* Elimination from Hf to Set is not allowed but from f to Set yes ! *)
 NewDestruct (f P).
-- 
cgit v1.2.3