From 49719da11fda90dda89c66fdddcc1ac9a23bb43e Mon Sep 17 00:00:00 2001
From: notin
Date: Thu, 6 Mar 2008 11:21:01 +0000
Subject: even_2n et odd_S2n deviennent transparents (chez moi, ça empêchait de
 compiler la contrib Nijmegen/QArith ?!)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10625 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Arith/Div2.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index 47e66e5b7f..1f8d13973b 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -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