From 7e12041ccfb5551e30bd5f400f726bd20d0f7b64 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 14 Oct 2008 14:05:04 +0000
Subject: ugly comment erroneously left in the minus definition

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

diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 27a8c5a916..8a5b195d18 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -47,7 +47,7 @@ Hint Resolve (f_equal pred): v62.
 
 Theorem pred_Sn : forall n:nat, n = pred (S n).
 Proof.
-  simpl; reflexivity.  
+  simpl; reflexivity.
 Qed.
 
 (** Injectivity of successor *)
@@ -165,16 +165,12 @@ Fixpoint minus (n m:nat) {struct n} : nat :=
   match n, m with
   | O, _ => n
   | S k, O => n
-(*=======
-
-  | O, _ => n
-  | S k, O => S k *)
   | S k, S l => k - l
   end
 
 where "n - m" := (minus n m) : nat_scope.
 
-(** Definition of the usual orders, the basic properties of [le] and [lt] 
+(** Definition of the usual orders, the basic properties of [le] and [lt]
     can be found in files Le and Lt *)
 
 Inductive le (n:nat) : nat -> Prop :=
-- 
cgit v1.2.3