- 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, 1 insertions, 1 deletions

diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index a3b102055..f5c3260de 100644
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -12,7 +12,7 @@
 <<
 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