diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-08-13 16:10:41 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-08-13 16:10:41 +0000 |
| commit | 7a63d8f5df7ae27038c6c770c22ee3911781de85 (patch) | |
| tree | 7b62e499eabb452b46e47e85c596597b590777c6 /theories/Logic/Berardi.v | |
| parent | 1e3ebfcda7a923d1c6f39eb64020f805deafba50 (diff) | |
Protection des commentaires pour coqtex et coqweb
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1897 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Logic/Berardi.v')
| -rw-r--r-- | theories/Logic/Berardi.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v index ca62faca6..3ddc2fc5e 100644 --- a/theories/Logic/Berardi.v +++ b/theories/Logic/Berardi.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -(* This file formalizes Berardi's paradox which says that in +(*i This file formalizes Berardi's paradox which says that in the calculus of constructions, excluded middle (EM) and axiom of choice (AC) implie proof irrelevenace (PI). Here, the axiom of choice is not necessary because of the use @@ -25,7 +25,7 @@ pages = {519-525} } - *) + i*) Require Elimdep. |