summaryrefslogtreecommitdiff
path: root/theories/Logic/Berardi.v
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@debian.org>2019-02-02 19:29:23 -0500
committerGravatar Benjamin Barenblat <bbaren@debian.org>2019-02-02 19:29:23 -0500
commit9ebf44d84754adc5b64fcf612c6816c02c80462d (patch)
treebf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /theories/Logic/Berardi.v
parent9043add656177eeac1491a73d2f3ab92bec0013c (diff)
Imported Upstream version 8.9.0upstream/8.9.0upstream
Diffstat (limited to 'theories/Logic/Berardi.v')
-rw-r--r--theories/Logic/Berardi.v7
1 files changed, 5 insertions, 2 deletions
diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v
index c6836a1c..ed4d69ab 100644
--- a/theories/Logic/Berardi.v
+++ b/theories/Logic/Berardi.v
@@ -82,7 +82,7 @@ End Retracts.
(** This lemma is basically a commutation of implication and existential
quantification: (EX x | A -> P(x)) <=> (A -> EX x | P(x))
which is provable in classical logic ( => is already provable in
- intuitionnistic logic). *)
+ intuitionistic logic). *)
Lemma L1 : forall A B:Prop, retract_cond (pow A) (pow B).
Proof.
@@ -136,7 +136,7 @@ trivial.
Qed.
-Theorem classical_proof_irrelevence : T = F.
+Theorem classical_proof_irrelevance : T = F.
Proof.
generalize not_has_fixpoint.
unfold Not_b.
@@ -148,4 +148,7 @@ intros not_true is_true.
elim not_true; trivial.
Qed.
+
+Notation classical_proof_irrelevence := classical_proof_irrelevance (compat "8.8").
+
End Berardis_paradox.