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, 19 insertions, 16 deletions

diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index d729253b3d..67218de837 100755
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -13,17 +13,17 @@ Require Lt.
 Require Gt.
 Require Decidable.
 
-Theorem zerop : (n:nat){n=O}+{lt O n}.
+Definition zerop : (n:nat){n=O}+{lt O n}.
 NewDestruct n; Auto with arith.
-Qed.
+Defined.
 
-Theorem lt_eq_lt_dec : (n,m:nat){(lt n m)}+{n=m}+{(lt m n)}.
+Definition lt_eq_lt_dec : (n,m:nat){(lt n m)}+{n=m}+{(lt m n)}.
 Proof.
 NewInduction n; NewInduction m; Auto with arith.
 Elim (IHn m).
 NewInduction 1; Auto with arith.
 Auto with arith.
-Qed.
+Defined.
 
 Lemma gt_eq_gt_dec : (n,m:nat)({(gt m n)}+{n=m})+{(gt n m)}.
 Proof lt_eq_lt_dec.
@@ -35,25 +35,28 @@ Auto with arith.
 NewInduction m.
 Auto with arith.
 Elim (IHn m); Auto with arith.
-Qed.
+Defined.
 
-Lemma le_le_S_dec : (n,m:nat) {le n m} + {le (S m) n}.
-Proof le_lt_dec.
+Definition le_le_S_dec : (n,m:nat) {le n m} + {le (S m) n}.
+Proof.
+Exact le_lt_dec.
+Defined.
 
-Lemma le_ge_dec : (n,m:nat) {le n m} + {ge n m}.
+Definition le_ge_dec : (n,m:nat) {le n m} + {ge n m}.
 Proof.
 Intros; Elim (le_lt_dec n m); Auto with arith.
-Qed.
-
-Theorem le_gt_dec : (n,m:nat){(le n m)}+{(gt n m)}.
-Proof le_lt_dec.
+Defined.
 
+Definition le_gt_dec : (n,m:nat){(le n m)}+{(gt n m)}.
+Proof.
+Exact le_lt_dec.
+Defined.
 
-Theorem le_lt_eq_dec : (n,m:nat)(le n m)->({(lt n m)}+{n=m}).
+Definition le_lt_eq_dec : (n,m:nat)(le n m)->({(lt n m)}+{n=m}).
 Proof.
 Intros; Elim (lt_eq_lt_dec n m); Auto with arith.
 Intros; Absurd (lt m n); Auto with arith.
-Qed.
+Defined.
 
 (** Proofs of decidability *)
 
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index 0cd20e0948..5263cb3757 100755
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -140,14 +140,14 @@ Proof.
   Intros. Discriminate H.
 Qed.
 
-Lemma plus_is_one : 
+Definition plus_is_one : 
       (m,n:nat) (m+n)=(S O) -> {m=O /\ n=(S O)}+{m=(S O) /\ n=O}.
 Proof.
   NewDestruct m; Auto.
   NewDestruct n; Auto.
   Intros. 
   Simpl in H. Discriminate H.
-Qed.
+Defined.
 
 Lemma plus_permute_2_in_4 : (a,b,c,d:nat) ((a+b)+(c+d))=((a+c)+(b+d)).
 Proof.