diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-08-03 17:43:13 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-08-03 17:43:13 +0000 |
| commit | 78b8f01fab336ac00d13c62771f5d7a4a1dcd8d1 (patch) | |
| tree | 844ced88a930aa5bdce0afc2db6ef6a70cd1f7a9 /theories/Logic/Berardi.v | |
| parent | ffe8426049f5d7d3e613b8c51c82a940994abbb4 (diff) | |
Typo
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6010 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 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. |