diff options
Diffstat (limited to 'theories/Logic')
| -rw-r--r-- | theories/Logic/Berardi.v | 7 | ||||
| -rw-r--r-- | theories/Logic/Diaconescu.v | 2 | ||||
| -rw-r--r-- | theories/Logic/EqdepFacts.v | 2 |
3 files changed, 6 insertions, 5 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. diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index 3317766c..66e82ddb 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -234,8 +234,6 @@ Qed. (** An alternative more concise proof can be done by directly using the guarded relational choice *) -Declare Implicit Tactic auto. - Lemma proof_irrel_rel_choice_imp_eq_dec' : a1=a2 \/ ~a1=a2. Proof. assert (decide: forall x:A, x=a1 \/ x=a2 -> diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index d938b315..8e59941f 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -125,7 +125,7 @@ Proof. apply eq_dep_intro. Qed. -Notation eq_sigS_eq_dep := eq_sigT_eq_dep (compat "8.6"). (* Compatibility *) +Notation eq_sigS_eq_dep := eq_sigT_eq_dep (compat "8.7"). (* Compatibility *) Lemma eq_dep_eq_sigT : forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q), |