From 1f195b9b69b12ace9152b5fc815417f29fe54245 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 28 May 2008 20:06:42 +0000
Subject: - Modification de la déf de minus et pred conformément aux remarques
 de   Assia et Benjamin W. de telle sorte qu'ils respectent le critère de  
 décroissance structurelle lorsqu'utilisés dans un point-fixe. - Ajout des
 noms "standard" des lemmes de Peano et correction d'un nom de   BinInt.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

(limited to 'theories/Init')

diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 4d468db71..b442a8e12 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -40,7 +40,7 @@ Hint Resolve (f_equal (A:=nat)): core.
 (** The predecessor function *)
 
 Definition pred (n:nat) : nat := match n with
-                                 | O => 0
+                                 | O => n
                                  | S u => u
                                  end.
 Hint Resolve (f_equal pred): v62.
@@ -123,6 +123,11 @@ Proof.
   auto.
 Qed.
 
+(** Standard associated names *)
+
+Notation plus_0_r_reverse := plus_n_O.
+Notation plus_succ_r_reverse := plus_n_Sm.
+
 (** Multiplication *)
 
 Fixpoint mult (n m:nat) {struct n} : nat :=
@@ -149,11 +154,16 @@ Proof.
 Qed.
 Hint Resolve mult_n_Sm: core v62.
 
+(** Standard associated names *)
+
+Notation mult_0_r_reverse := mult_n_O.
+Notation mult_succ_r_reverse := mult_n_Sm.
+
 (** Truncated subtraction: [m-n] is [0] if [n>=m] *)
 
 Fixpoint minus (n m:nat) {struct n} : nat :=
   match n, m with
-  | O, _ => 0
+  | O, _ => n
   | S k, O => S k
   | S k, S l => k - l
   end
@@ -211,5 +221,3 @@ Proof.
   induction n; auto.
   destruct m as [| n0]; auto.
 Qed.
-
-(** Notations *)
-- 
cgit v1.2.3