From 1922c8a403f4d4686efe6115eecf7f56121e99da Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 2 Nov 2003 21:14:57 +0000 Subject: Renommage bool en boolP pour eviter la qualification git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4770 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Logic/ClassicalFacts.v | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index 44f09c2655..bedbc4cbd1 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -189,16 +189,16 @@ End Proof_irrelevance_CC. Section Proof_irrelevance_CIC. -Inductive bool : Prop := true : bool | false : bool. -Definition bool_elim_redl : (C:Prop)(c1,c2:C)c1==(bool_ind C c1 c2 true) +Inductive boolP : Prop := trueP : boolP | falseP : boolP. +Definition boolP_elim_redl : (C:Prop)(c1,c2:C)c1==(boolP_ind C c1 c2 trueP) := [C;c1,c2](refl_eqT C c1). -Definition bool_elim_redr : (C:Prop)(c1,c2:C)c2==(bool_ind C c1 c2 false) +Definition boolP_elim_redr : (C:Prop)(c1,c2:C)c2==(boolP_ind C c1 c2 falseP) := [C;c1,c2](refl_eqT C c2). -Scheme bool_indd := Induction for bool Sort Prop. +Scheme boolP_indd := Induction for boolP Sort Prop. Lemma ext_prop_dep_proof_irrel_cic : prop_extensionality -> proof_irrelevance. -Proof [pe](ext_prop_dep_proof_irrel_gen bool true false bool_ind - bool_elim_redl bool_elim_redr pe bool_indd). +Proof [pe](ext_prop_dep_proof_irrel_gen boolP trueP falseP boolP_ind + boolP_elim_redl boolP_elim_redr pe boolP_indd). End Proof_irrelevance_CIC. @@ -212,4 +212,3 @@ End Proof_irrelevance_CIC. (nor dependent case analysis). This would imply that the previous results cannot be refined. *) - -- cgit v1.2.3