From 1f0f0a2b3e0128c8e5deb028fe73fcaf5adc900a Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 26 May 2008 18:34:55 +0000
Subject: Int31 : gcd31 was wrong

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10995 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Numbers/Cyclic/Int31/Int31.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index 5f0a874101..ba40ffd87c 100644
--- a/theories/Numbers/Cyclic/Int31/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
@@ -352,7 +352,7 @@ Definition gcd31 (i j:int31) :=
             | _ => euler p j (let (_, r ) := i/j in r)
             end
    end)
-  size i j.
+  (2*size)%nat i j.
 
 Definition sqrt31 (i:int31) : int31 :=
   match i ?= On with
-- 
cgit v1.2.3