Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 9 insertions, 9 deletions

diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
index 28d40094..88cbb484 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
@@ -8,12 +8,12 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id: DoubleType.v 10964 2008-05-22 11:08:13Z letouzey $ i*)
+(*i $Id$ i*)
 
 Set Implicit Arguments.
 
 Require Import ZArith.
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
 Definition base digits := Zpower 2 (Zpos digits).
 
@@ -37,10 +37,10 @@ Section Zn2Z.
 
  Variable znz : Type.
 
- (** From a type [znz] representing a cyclic structure Z/nZ, 
+ (** From a type [znz] representing a cyclic structure Z/nZ,
      we produce a representation of Z/2nZ by pairs of elements of [znz]
-     (plus a special case for zero). High half of the new number comes 
-     first. 
+     (plus a special case for zero). High half of the new number comes
+     first.
  *)
 
  Inductive zn2z :=
@@ -57,10 +57,10 @@ End Zn2Z.
 
 Implicit Arguments W0 [znz].
 
-(** From a cyclic representation [w], we iterate the [zn2z] construct 
-    [n] times, gaining the type of binary trees of depth at most [n], 
-    whose leafs are either W0 (if depth < n) or elements of w 
-    (if depth = n). 
+(** From a cyclic representation [w], we iterate the [zn2z] construct
+    [n] times, gaining the type of binary trees of depth at most [n],
+    whose leafs are either W0 (if depth < n) or elements of w
+    (if depth = n).
 *)
 
 Fixpoint word (w:Type) (n:nat) : Type :=