- 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.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11015 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 12 insertions, 4 deletions

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 *)