From 14644b3968658a30dffd6aa5d45f2765b5e6e72f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 5 Mar 2006 21:53:02 +0000
Subject: Commentaires

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

(limited to 'theories')

diff --git a/theories/Logic/Classical_Pred_Type.v b/theories/Logic/Classical_Pred_Type.v
index ef4e89793f..ce94bec14f 100755
--- a/theories/Logic/Classical_Pred_Type.v
+++ b/theories/Logic/Classical_Pred_Type.v
@@ -40,7 +40,7 @@ Qed.
 
 Lemma not_ex_all_not :
  forall P:U -> Prop, ~ (exists n : U, P n) -> forall n:U, ~ P n.
-Proof.
+Proof. (* Intuitionistic *)
 unfold not in |- *; intros P notex n abs.
 apply notex.
 exists n; trivial.
@@ -56,14 +56,14 @@ Qed.
 
 Lemma ex_not_not_all :
  forall P:U -> Prop, (exists n : U, ~ P n) -> ~ (forall n:U, P n).
-Proof.
+Proof. (* Intuitionistic *)
 unfold not in |- *; intros P exnot allP.
 elim exnot; auto.
 Qed.
 
 Lemma all_not_not_ex :
  forall P:U -> Prop, (forall n:U, ~ P n) -> ~ (exists n : U, P n).
-Proof.
+Proof. (* Intuitionistic *)
 unfold not in |- *; intros P allnot exP; elim exP; intros n p.
 apply allnot with n; auto.
 Qed.
-- 
cgit v1.2.3