From f7cf56828fc12726cc1802ea8b2ec1eb709be03c Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 17 Dec 2010 21:00:36 +0000
Subject: NPeano.modulo : another trick a la "minus" for having a decreasing
 arg

 By writing y instead of 0 in the branch where y is 0,
 Coq can see that (modulo x y) is a structural subterm of y
 (but not necessarily a strict one).

 Same trick for div, but here it doesn't help.

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

diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 277223f4bc..98809fbf8f 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -101,13 +101,13 @@ Fixpoint divmod x y q u :=
 
 Definition div x y :=
   match y with
-    | 0 => 0
+    | 0 => y
     | S y' => fst (divmod x y' 0 y')
   end.
 
 Definition modulo x y :=
   match y with
-    | 0 => 0
+    | 0 => y
     | S y' => y' - snd (divmod x y' 0 y')
   end.
 
-- 
cgit v1.2.3