Making the sumbool functions transparent, so that they can used to

compute even inside Coq.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2846 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 17 insertions, 16 deletions

diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 9cb4c1bb2..f2c9bfc8e 100755
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -260,9 +260,10 @@ Lemma orb_true_b : (b:bool)(orb true b)=true.
 Trivial with bool.
 Qed.
 
-Lemma orb_true_elim : (b1,b2:bool)(orb b1 b2)=true -> {b1=true}+{b2=true}.
+Definition orb_true_elim : (b1,b2:bool)(orb b1 b2)=true -> {b1=true}+{b2=true}.
 NewDestruct b1; Simpl; Auto with bool.
-Qed.
+Defined.
+
 Lemma orb_false_intro 
     : (b1,b2:bool)(b1=false)->(b2=false)->(orb b1 b2)=false.
 Intros b1 b2 H1 H2; Rewrite H1; Rewrite H2; Trivial with bool.
@@ -374,10 +375,10 @@ Lemma andb_true_b : (b:bool)(andb true b)=b.
 Trivial with bool.
 Qed.
 
-Lemma andb_false_elim : 
+Definition andb_false_elim : 
     (b1,b2:bool)(andb b1 b2)=false -> {b1=false}+{b2=false}.
 NewDestruct b1; Simpl; Auto with bool.
-Qed.
+Defined.
 Hints Resolve andb_false_elim : bool v62.
 
 Lemma andb_neg_b :
diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v
index 84e74f86b..6f3adcf32 100644
--- a/theories/Bool/Sumbool.v
+++ b/theories/Bool/Sumbool.v
@@ -15,22 +15,22 @@
 
 (** A boolean is either [true] or [false], and this is decidable *)
 
-Lemma sumbool_of_bool : (b:bool) {b=true}+{b=false}.
+Definition sumbool_of_bool : (b:bool) {b=true}+{b=false}.
 Proof.
   Induction b; Auto.
-Qed.
+Defined.
 
 Hints Resolve sumbool_of_bool : bool.
 
-Lemma bool_eq_rec : (b:bool)(P:bool->Set)
+Definition bool_eq_rec : (b:bool)(P:bool->Set)
                     ((b=true)->(P true))->((b=false)->(P false))->(P b).
 Induction b; Auto.
-Qed.
+Defined.
 
-Lemma bool_eq_ind : (b:bool)(P:bool->Prop)
+Definition bool_eq_ind : (b:bool)(P:bool->Prop)
                     ((b=true)->(P true))->((b=false)->(P false))->(P b).
 Induction b; Auto.
-Qed.
+Defined.
 
 
 (*i pourquoi ce machin-la est dans BOOL et pas dans LOGIC ?  Papageno i*)
@@ -44,20 +44,20 @@ Variables A,B,C,D : Prop.
 Hypothesis H1 : {A}+{B}.
 Hypothesis H2 : {C}+{D}.
 
-Lemma sumbool_and : {A/\C}+{B\/D}.
+Definition sumbool_and : {A/\C}+{B\/D}.
 Proof.
 Case H1; Case H2; Auto.
-Qed.
+Defined.
 
-Lemma sumbool_or : {A\/C}+{B/\D}.
+Definition sumbool_or : {A\/C}+{B/\D}.
 Proof.
 Case H1; Case H2; Auto.
-Qed.
+Defined.
 
-Lemma sumbool_not : {B}+{A}.
+Definition sumbool_not : {B}+{A}.
 Proof.
 Case H1; Auto.
-Qed.
+Defined.
 
 End connectives.