diff options
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 ca62faca6f..3ddc2fc5ed 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. |