BigNum: more reorganization, mainly moves GenXYZ to DoubleXYZ

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

2 files changed, 8 insertions, 8 deletions

diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
index 7cc4e54346..df3af4b63b 100644
--- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v
+++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
@@ -12,8 +12,8 @@
 
 Require Export NZAxioms.
 Require Import BigNumPrelude.
-Require Import Basic_type.
-Require Import ZnZ.
+Require Import DoubleType.
+Require Import Z_nZ.
 
 (** * A Z/nZ representation (module type [CyclicType]) implements 
   [NZAxiomsSig], e.g. the common properties between N and Z. *)
diff --git a/theories/Numbers/Cyclic/Abstract/ZnZ.v b/theories/Numbers/Cyclic/Abstract/Z_nZ.v
index 9ec7648e61..6d19e6613c 100644
--- a/theories/Numbers/Cyclic/Abstract/ZnZ.v
+++ b/theories/Numbers/Cyclic/Abstract/Z_nZ.v
@@ -17,13 +17,13 @@ Set Implicit Arguments.
 Require Import ZArith.
 Require Import Znumtheory.
 Require Import BigNumPrelude.
-Require Import Basic_type.
+Require Import DoubleType.
 
 Open Local Scope Z_scope.
 
-(** First, a description via operator records and spec records. *)
+(** First, a description via an operator record and a spec record. *)
 
-Section ZnZ_Op.
+Section Z_nZ_Op.
 
  Variable znz : Set.
 
@@ -90,9 +90,9 @@ Section ZnZ_Op.
     znz_sqrt2       : znz -> znz -> znz * carry znz;
     znz_sqrt        : znz -> znz  }.
 
-End ZnZ_Op.
+End Z_nZ_Op.
 
-Section ZnZ_Spec.
+Section Z_nZ_Spec.
  Variable w : Set.
  Variable w_op : znz_op w.
 
@@ -270,7 +270,7 @@ Section ZnZ_Spec.
        [|w_sqrt x|] ^ 2 <= [|x|] < ([|w_sqrt x|] + 1) ^ 2
   }.
 
-End ZnZ_Spec.
+End Z_nZ_Spec.