From 50d28541dcb024d8c63fd1b9e770536fc75e325b Mon Sep 17 00:00:00 2001
From: glondu
Date: Wed, 17 Aug 2011 15:28:46 +0000
Subject: Give inner fixpoint of gcd31 a name, to avoid excessive unfolding

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

diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index d2e6c70b92..20f750f643 100644
--- a/theories/Numbers/Cyclic/Int31/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
@@ -349,16 +349,16 @@ Register div31 as int31 div in "coq_int31" by True.
 Register compare31 as int31 compare in "coq_int31" by True.
 Register addmuldiv31 as int31 addmuldiv in "coq_int31" by True.
 
-Definition gcd31 (i j:int31) :=
-  (fix euler (guard:nat) (i j:int31) {struct guard} :=
-   match guard with
-   | O => In
-   | S p => match j ?= On with
-            | Eq => i
-            | _ => euler p j (let (_, r ) := i/j in r)
-            end
-   end)
-  (2*size)%nat i j.
+Fixpoint euler (guard:nat) (i j:int31) {struct guard} :=
+  match guard with
+    | O => In
+    | S p => match j ?= On with
+               | Eq => i
+               | _ => euler p j (let (_, r ) := i/j in r)
+             end
+  end.
+
+Definition gcd31 (i j:int31) := euler (2*size)%nat i j.
 
 (** Square root functions using newton iteration
     we use a very naive upper-bound on the iteration
-- 
cgit v1.2.3