From 0a64c8ac6a9be66c7cbfe5c110b480e0abbce638 Mon Sep 17 00:00:00 2001
From: thery
Date: Tue, 15 May 2007 15:02:08 +0000
Subject: pos_mod fixed

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9824 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Ints/BigN.v | 18 +++++++++++++-----
 1 file changed, 13 insertions(+), 5 deletions(-)

diff --git a/theories/Ints/BigN.v b/theories/Ints/BigN.v
index 47a58e278c..2ad6ef0307 100644
--- a/theories/Ints/BigN.v
+++ b/theories/Ints/BigN.v
@@ -66,11 +66,19 @@ Definition int31_op : znz_op int31.
  
  (* shift operations *)
  exact (fun p => let (_,i) := positive_to_int31 p in addmuldiv31 i). (*add_mul_div with positive ? *)
- exact (fun p i => let (n,j) := positive_to_int31 p in (*modulo 2^p (p positive) *)
-                             match n with
-                             | N0 => let (_,r) := i/j in r
-                             | _ => i
-                             end).
+(*modulo 2^p (p positive) *)
+ exact (fun p i => 
+   let (n,j) := positive_to_int31 p in 
+   match n with
+   | N0 => 
+     match compare31 j 32 with
+     | Lt => addmuldiv31 j 0 (addmuldiv31 (31-j) i 0)
+     | _ => i
+     end
+   | _ => i
+   end).
+
+
  (* is i even ? *)
  exact (fun i => let (_,r) := i/2 in 
                           match r ?= 0 with
-- 
cgit v1.2.3