Minor improvement: group stuff about carry apart from stuff about zn2z

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10944 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 6 deletions

diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
index 95f3c88e6..dfc8b4e32 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
@@ -25,6 +25,12 @@ Section Carry.
   | C0 : A -> carry
   | C1 : A -> carry.
 
+ Definition interp_carry (sign:Z)(B:Z)(interp:A -> Z) c :=
+  match c with
+  | C0 x => interp x
+  | C1 x => sign*B + interp x
+  end.
+
 End Carry.
 
 Section Zn2Z.
@@ -47,12 +53,6 @@ Section Zn2Z.
   | WW xh xl => w_to_Z xh * wB + w_to_Z xl
   end.
 
- Definition interp_carry sign B (interp:znz -> Z) c :=
-  match c with
-  | C0 x => interp x
-  | C1 x => sign*B + interp x
-  end.
-
 End Zn2Z.
 
 Implicit Arguments W0 [znz].