From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 25 Jul 2008 15:12:53 +0200
Subject: Imported Upstream version 8.2~beta3+dfsg

---
 theories/Arith/Div2.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'theories/Arith/Div2.v')

diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index c32759b2..1216a545 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Div2.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Div2.v 10625 2008-03-06 11:21:01Z notin $ i*)
 
 Require Import Lt.
 Require Import Plus.
@@ -169,12 +169,12 @@ Hint Resolve even_double double_even odd_double double_odd: arith.
 Lemma even_2n : forall n, even n -> {p : nat | n = double p}.
 Proof.
   intros n H. exists (div2 n). auto with arith.
-Qed.
+Defined.
 
 Lemma odd_S2n : forall n, odd n -> {p : nat | n = S (double p)}.
 Proof.
   intros n H. exists (div2 n). auto with arith.
-Qed.
+Defined.
 
 (** Doubling before dividing by two brings back to the initial number. *)
 
-- 
cgit v1.2.3