4 files changed, 18 insertions, 10 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/Z_nZ.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index 6d19e6613..ed14cc799 100644
--- a/theories/Numbers/Cyclic/Abstract/Z_nZ.v
+++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
@@ -12,6 +12,9 @@
 
 (** * Signature and specification of a bounded integer structure *)
 
+(** This file specifies how to represent [Z/nZ] when [n=2^d], 
+    [d] being the number of digits of these bounded integers. *) 
+
 Set Implicit Arguments.
 
 Require Import ZArith.
@@ -30,7 +33,7 @@ Section Z_nZ_Op.
  Record znz_op : Set := mk_znz_op {
 
     (* Conversion functions with Z *)
-    znz_digits : positive;
+    znz_digits : positive;  
     znz_zdigits: znz;
     znz_to_Z   : znz -> Z;
     znz_of_pos : positive -> N * znz;
@@ -40,7 +43,7 @@ Section Z_nZ_Op.
     (* Basic constructors *)
     znz_0   : znz;
     znz_1   : znz;
-    znz_Bm1 : znz;
+    znz_Bm1 : znz;  (* [2^digits-1], which is equivalent to [-1] *)
     znz_WW  : znz -> znz -> zn2z znz;
     znz_W0  : znz -> zn2z znz;
     znz_0W  : znz -> zn2z znz;
diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
index df3af4b63..2d23a12dd 100644
--- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v
+++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
@@ -13,10 +13,15 @@
 Require Export NZAxioms.
 Require Import BigNumPrelude.
 Require Import DoubleType.
-Require Import Z_nZ.
+Require Import CyclicAxioms.
 
-(** * A Z/nZ representation (module type [CyclicType]) implements 
-  [NZAxiomsSig], e.g. the common properties between N and Z. *)
+(** * From [CyclicType] to [NZAxiomsSig] *)
+
+(** A [Z/nZ] representation given by a module type [CyclicType] 
+    implements [NZAxiomsSig], e.g. the common properties between 
+    N and Z with no ordering. Notice that the [n] in [Z/nZ] is 
+    a power of 2.
+*)
 
 Module NZCyclicAxiomsMod (Import Cyclic : CyclicType) <: NZAxiomsSig.
 
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/Z_2nZ.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
index 26d2393f9..54ff3d354 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/Z_2nZ.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
@@ -23,7 +23,7 @@ Require Import DoubleSqrt.
 Require Import DoubleLift.
 Require Import DoubleDivn1.
 Require Import DoubleDiv. 
-Require Import Z_nZ.
+Require Import CyclicAxioms.
 
 Open Local Scope Z_scope.
 
diff --git a/theories/Numbers/Cyclic/Int31/Z_31Z.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index 3b5944ed3..49a1a0b5b 100644
--- a/theories/Numbers/Cyclic/Int31/Z_31Z.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -8,14 +8,14 @@
 
 (*i $Id$ i*)
 
-(** * Int31 numbers defines indeed a cyclic structure : Z/31Z *)
+(** * Int31 numbers defines indeed a cyclic structure : Z/(2^31)Z *)
 
 (**
 Author: Arnaud Spiwack
 *)
 
 Require Export Int31.
-Require Import Z_nZ.
+Require Import CyclicAxioms.
 
 Open Scope int31_scope.
 
@@ -107,8 +107,8 @@ Definition int31_spec : znz_spec int31_op.
 Admitted.
 
 
-Module Int31_words <: CyclicType.
+Module Int31Cyclic <: CyclicType.
   Definition w := int31.
   Definition w_op := int31_op.
   Definition w_spec := int31_spec.
-End Int31_words.
+End Int31Cyclic.