diff options
Diffstat (limited to 'theories')
| -rwxr-xr-x | theories/Arith/Arith.v | 3 | ||||
| -rw-r--r-- | theories/Logic/Berardi.v | 4 |
2 files changed, 3 insertions, 4 deletions
diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v index 3f1292765..b076de2af 100755 --- a/theories/Arith/Arith.v +++ b/theories/Arith/Arith.v @@ -15,7 +15,6 @@ Require Export Gt. Require Export Minus. Require Export Mult. Require Export Between. -Require Export Minus. Require Export Peano_dec. Require Export Compare_dec. -Require Export Factorial.
\ No newline at end of file +Require Export Factorial. diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v index cc38078f2..f612e92d2 100644 --- a/theories/Logic/Berardi.v +++ b/theories/Logic/Berardi.v @@ -10,7 +10,7 @@ (** 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). + choice (AC) imply proof irrelevance (PI). Here, the axiom of choice is not necessary because of the use of inductive types. << @@ -156,4 +156,4 @@ intros not_true is_true. elim not_true; trivial. Qed. -End Berardis_paradox.
\ No newline at end of file +End Berardis_paradox. |