From be670deace370127c44e1ee3583e61ed6492382a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 20 Dec 2000 19:48:10 +0000
Subject: Oublié de supprimer du code mort

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

diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index 202e7a97a8..f5e7ebb34b 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -118,13 +118,6 @@ Simpl. Rewrite (double_S (div2 n0)). Intro H. Injection H. Auto with arith.
 Intro H. Inversion H. Inversion H1.
 Simpl. Rewrite (double_S (div2 n0)). Auto with arith.
 Simpl. Rewrite (double_S (div2 n0)). Intro H. Injection H. Auto with arith.
-(*
-Simpl. Rewrite <- plus_n_Sm. Auto with arith.
-Simpl. Rewrite <- plus_n_Sm. Intro H. Injection H. Auto with arith.
-Intro H. Inversion H. Inversion H1.
-Simpl. Rewrite <- plus_n_Sm. Auto with arith.
-Simpl. Rewrite <- plus_n_Sm. Intro H. Injection H. Auto with arith.
-*)
 Qed.
 
 
-- 
cgit v1.2.3