Filename ZnZ (or Z_nZ in a later attempt) is neither pretty nor accurate

(n _must_ in fact be a power of 2). Worse: Z_31Z is just plain wrong
since it is Z/(2^31)Z and not Z/31Z (my fault). 

As a consequence, switch to CyclicAxioms, Cyclic31, DoubleCyclic, etc



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

2 files changed, 13 insertions, 5 deletions

diff --git a/theories/Numbers/Cyclic/Abstract/Z_nZ.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index 6d19e6613c..ed14cc7992 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 df3af4b63b..2d23a12dda 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.