Delete trailing whitespaces in all *.{v,ml*} files

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

2 files changed, 124 insertions, 124 deletions

diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index 7424d877b..c22680be3 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -15,7 +15,7 @@
 
 (*s The two parameters that control the generation: *)
 
-let size = 6 (* how many times should we repeat the Z/nZ --> Z/2nZ 
+let size = 6 (* how many times should we repeat the Z/nZ --> Z/2nZ
                 process before relying on a generic construct *)
 let gen_proof = true  (* should we generate proofs ? *)
 
@@ -27,18 +27,18 @@ let c = "N"
 let pz n = if n == 0 then "w_0" else "W0"
 let rec gen2 n = if n == 0 then "1" else if n == 1 then "2"
                  else "2 * " ^ (gen2 (n - 1))
-let rec genxO n s = 
+let rec genxO n s =
   if n == 0 then s else " (xO" ^ (genxO (n - 1) s) ^ ")"
 
-(* NB: in ocaml >= 3.10, we could use Printf.ifprintf for printing to 
-   /dev/null, but for being compatible with earlier ocaml and not 
-   relying on system-dependent stuff like open_out "/dev/null", 
+(* NB: in ocaml >= 3.10, we could use Printf.ifprintf for printing to
+   /dev/null, but for being compatible with earlier ocaml and not
+   relying on system-dependent stuff like open_out "/dev/null",
    let's use instead a magical hack *)
 
 (* Standard printer, with a final newline *)
 let pr s = Printf.printf (s^^"\n")
 (* Printing to /dev/null *)
-let pn = (fun s -> Obj.magic (fun _ _ _ _ _ _ _ _ _ _ _ _ _ _ -> ()) 
+let pn = (fun s -> Obj.magic (fun _ _ _ _ _ _ _ _ _ _ _ _ _ _ -> ())
 	  : ('a, out_channel, unit) format -> 'a)
 (* Proof printer : prints iff gen_proof is true *)
 let pp = if gen_proof then pr else pn
@@ -51,7 +51,7 @@ let pp0 = if gen_proof then pr0 else pn
 
 (*s The actual printing *)
 
-let _ = 
+let _ =
 
   pr "(************************************************************************)";
   pr "(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)";
@@ -67,7 +67,7 @@ let _ =
   pr "";
   pr "(** From a cyclic Z/nZ representation to arbitrary precision natural numbers.*)";
   pr "";
-  pr "(** Remark: File automatically generated by NMake_gen.ml, DO NOT EDIT ! *)"; 
+  pr "(** Remark: File automatically generated by NMake_gen.ml, DO NOT EDIT ! *)";
   pr "";
   pr "Require Import BigNumPrelude.";
   pr "Require Import ZArith.";
@@ -132,7 +132,7 @@ let _ =
   pr "";
 
   pr " Inductive %s_ :=" t;
-  for i = 0 to size do 
+  for i = 0 to size do
     pr "  | %s%i : w%i -> %s_" c i i t
   done;
   pr "  | %sn : forall n, word w%i (S n) -> %s_." c size t;
@@ -167,7 +167,7 @@ let _ =
 
   pr " Definition to_N x := Zabs_N (to_Z x).";
   pr "";
-  
+
   pr " Definition eq x y := (to_Z x = to_Z y).";
   pr "";
 
@@ -191,7 +191,7 @@ let _ =
   for i = 0 to size do
     pp " Let nmake_op%i := nmake_op _ w%i_op." i i;
     pp " Let eval%in n := znz_to_Z  (nmake_op%i n)." i i;
-    if i == 0 then 
+    if i == 0 then
       pr " Let extend%i := DoubleBase.extend  (WW w_0)." i
     else
       pr " Let extend%i := DoubleBase.extend  (WW (W0: w%i))." i i;
@@ -280,7 +280,7 @@ let _ =
 
   pp " Let w0_spec: znz_spec w0_op := W0.w_spec.";
   for i = 1 to 3 do
-    pp " Let w%i_spec: znz_spec w%i_op := mk_znz2_spec w%i_spec." i i (i-1) 
+    pp " Let w%i_spec: znz_spec w%i_op := mk_znz2_spec w%i_spec." i i (i-1)
   done;
   for i = 4 to size + 3 do
     pp " Let w%i_spec : znz_spec w%i_op := mk_znz2_karatsuba_spec w%i_spec." i i (i-1)
@@ -309,14 +309,14 @@ let _ =
 
 
   for i = 0 to size do
-    pp " Theorem digits_w%i:  znz_digits w%i_op = znz_digits (nmake_op _ w0_op %i)." i i i; 
+    pp " Theorem digits_w%i:  znz_digits w%i_op = znz_digits (nmake_op _ w0_op %i)." i i i;
     if i == 0 then
       pp " auto."
     else
       pp " rewrite digits_nmake; rewrite <- digits_w%i; auto." (i - 1);
     pp " Qed.";
     pp "";
-    pp " Let spec_double_eval%in: forall n, eval%in n = DoubleBase.double_to_Z (znz_digits w%i_op) (znz_to_Z w%i_op) n." i i i i; 
+    pp " Let spec_double_eval%in: forall n, eval%in n = DoubleBase.double_to_Z (znz_digits w%i_op) (znz_to_Z w%i_op) n." i i i i;
     pp " Proof.";
     pp "  intros n; exact (nmake_double n w%i w%i_op)." i i;
     pp " Qed.";
@@ -325,7 +325,7 @@ let _ =
 
   for i = 0 to size do
     for j = 0 to (size - i) do
-      pp " Theorem digits_w%in%i: znz_digits w%i_op = znz_digits (nmake_op _ w%i_op %i)." i j (i + j) i j; 
+      pp " Theorem digits_w%in%i: znz_digits w%i_op = znz_digits (nmake_op _ w%i_op %i)." i j (i + j) i j;
       pp " Proof.";
       if j == 0 then
         if i == 0 then
@@ -346,7 +346,7 @@ let _ =
         end;
       pp " Qed.";
       pp "";
-      pp " Let spec_eval%in%i: forall x, [%s%i x] = eval%in %i x." i j c (i + j) i j; 
+      pp " Let spec_eval%in%i: forall x, [%s%i x] = eval%in %i x." i j c (i + j) i j;
       pp " Proof.";
       if j == 0 then
         pp " intros x; rewrite spec_double_eval%in; unfold DoubleBase.double_to_Z, to_Z; auto." i
@@ -363,7 +363,7 @@ let _ =
       pp " Qed.";
       if i + j <> size  then
         begin
-          pp " Let spec_extend%in%i: forall x, [%s%i x] = [%s%i (extend%i %i x)]." i (i + j + 1) c i c (i + j + 1) i j; 
+          pp " Let spec_extend%in%i: forall x, [%s%i x] = [%s%i (extend%i %i x)]." i (i + j + 1) c i c (i + j + 1) i j;
           if j == 0 then
             begin
               pp " intros x; change (extend%i 0 x) with (WW (znz_0 w%i_op) x)." i (i + j);
@@ -393,7 +393,7 @@ let _ =
     pp " Qed.";
     pp "";
 
-    pp " Let spec_eval%in%i: forall x, [%sn 0  x] = eval%in %i x." i (size - i + 1) c i (size - i + 1); 
+    pp " Let spec_eval%in%i: forall x, [%sn 0  x] = eval%in %i x." i (size - i + 1) c i (size - i + 1);
     pp " Proof.";
     pp " intros x; case x.";
     pp "   auto.";
@@ -405,7 +405,7 @@ let _ =
     pp " Qed.";
     pp "";
 
-    pp " Let spec_eval%in%i: forall x, [%sn 1  x] = eval%in %i x." i (size - i + 2) c i (size - i + 2); 
+    pp " Let spec_eval%in%i: forall x, [%sn 1  x] = eval%in %i x." i (size - i + 2) c i (size - i + 2);
     pp " intros x; case x.";
     pp "   auto.";
     pp " intros xh xl; unfold to_Z; rewrite znz_to_Z_%i." (size + 2);
@@ -430,7 +430,7 @@ let _ =
   pp " Qed.";
   pp "";
 
-  pp " Let spec_eval%in: forall n x, [%sn n x] = eval%in (S n) x." size c size; 
+  pp " Let spec_eval%in: forall n x, [%sn n x] = eval%in (S n) x." size c size;
   pp " intros n; elim n; clear n.";
   pp "   exact spec_eval%in1." size;
   pp " intros n Hrec x; case x; clear x.";
@@ -446,7 +446,7 @@ let _ =
   pp " Qed.";
   pp "";
 
-  pp " Let spec_extend%in: forall n x, [%s%i x] = [%sn n (extend%i n x)]." size c size c size ; 
+  pp " Let spec_extend%in: forall n x, [%s%i x] = [%sn n (extend%i n x)]." size c size c size ;
   pp " intros n; elim n; clear n.";
   pp "   intros x; change (extend%i 0 x) with (WW (znz_0 w%i_op) x)." size size;
   pp "   unfold to_Z.";
@@ -578,14 +578,14 @@ let _ =
       pr "  | %s%i wx, %s%i wy => f%i (extend%i %i wx) wy" c i c j j i (j - i - 1);
     done;
     if i == size then
-      pr "  | %s%i wx, %sn m wy => fnn m (extend%i m wx) wy" c size c size 
-    else 
+      pr "  | %s%i wx, %sn m wy => fnn m (extend%i m wx) wy" c size c size
+    else
       pr "  | %s%i wx, %sn m wy => fnn m (extend%i m (extend%i %i wx)) wy" c i c size i (size - i - 1);
   done;
   for i = 0 to size do
     if i == size then
-      pr "  | %sn n wx, %s%i wy => fnn n wx (extend%i n wy)" c c size size 
-    else 
+      pr "  | %sn n wx, %s%i wy => fnn n wx (extend%i n wy)" c c size size
+    else
       pr "  | %sn n wx, %s%i wy => fnn n wx (extend%i n (extend%i %i wy))" c c i size i (size - i - 1);
   done;
   pr "  | %sn n wx, Nn m wy =>" c;
@@ -611,14 +611,14 @@ let _ =
     done;
     if i == size then
       pp "     intros m y; rewrite (spec_extend%in m); apply Pfnn." size
-    else 
+    else
       pp "     intros m y; rewrite spec_extend%in%i; rewrite (spec_extend%in m); apply Pfnn." i size size;
   done;
   pp "    intros n x y; case y; clear y.";
   for i = 0 to size do
     if i == size then
       pp "    intros y; rewrite (spec_extend%in n); apply Pfnn." size
-    else 
+    else
       pp "    intros y; rewrite spec_extend%in%i; rewrite (spec_extend%in n); apply Pfnn." i size size;
   done;
   pp "    intros m y; rewrite <- (spec_cast_l n m x); ";
@@ -644,7 +644,7 @@ let _ =
     pr "    match y with";
     for j = 0 to i - 1 do
       pr "    | %s%i wy =>" c j;
-      if j == 0 then 
+      if j == 0 then
         pr "       if w0_eq0 wy then ft0 x else";
       pr "       f%i wx (extend%i %i wy)" i j (i - j -1);
     done;
@@ -653,8 +653,8 @@ let _ =
       pr "    | %s%i wy => f%i (extend%i %i wx) wy" c j j i (j - i - 1);
     done;
     if i == size then
-      pr "    | %sn m wy => fnn m (extend%i m wx) wy" c size 
-    else 
+      pr "    | %sn m wy => fnn m (extend%i m wx) wy" c size
+    else
       pr "    | %sn m wy => fnn m (extend%i m (extend%i %i wx)) wy" c size i (size - i - 1);
     pr"    end";
   done;
@@ -665,8 +665,8 @@ let _ =
     if i == 0 then
       pr "      if w0_eq0 wy then ft0 x else";
     if i == size then
-      pr "      fnn n wx (extend%i n wy)" size 
-    else 
+      pr "      fnn n wx (extend%i n wy)" size
+    else
       pr "      fnn n wx (extend%i n (extend%i %i wy))" size i (size - i - 1);
   done;
   pr "        | %sn m wy =>" c;
@@ -707,7 +707,7 @@ let _ =
     done;
     if i == size then
       pp "     intros m y; rewrite (spec_extend%in m); apply Pfnn." size
-    else 
+    else
       pp "     intros m y; rewrite spec_extend%in%i; rewrite (spec_extend%in m); apply Pfnn." i size size;
   done;
   pp "    intros n x y; case y; clear y.";
@@ -721,7 +721,7 @@ let _ =
       end;
     if i == size then
       pp "    rewrite (spec_extend%in n); apply Pfnn." size
-    else 
+    else
       pp "    rewrite spec_extend%in%i; rewrite (spec_extend%in n); apply Pfnn." i size size;
   done;
   pp "  intros m y; rewrite <- (spec_cast_l n m x); ";
@@ -748,14 +748,14 @@ let _ =
       pr "  | %s%i wx, %s%i wy => f%in %i wx wy" c i c j i (j - i - 1);
     done;
     if i == size then
-      pr "  | %s%i wx, %sn m wy => f%in m wx wy" c size c size 
-    else 
+      pr "  | %s%i wx, %sn m wy => f%in m wx wy" c size c size
+    else
       pr "  | %s%i wx, %sn m wy => f%in m (extend%i %i wx) wy" c i c size i (size - i - 1);
   done;
   for i = 0 to size do
     if i == size then
-      pr "  | %sn n wx, %s%i wy => fn%i n wx wy" c c size size 
-    else 
+      pr "  | %sn n wx, %s%i wy => fn%i n wx wy" c c size size
+    else
       pr "  | %sn n wx, %s%i wy => fn%i n wx (extend%i %i wy)" c c i size i (size - i - 1);
   done;
   pr "  | %sn n wx, %sn m wy => fnm n m wx wy" c c;
@@ -779,14 +779,14 @@ let _ =
     done;
     if i == size then
       pp "     intros m y; rewrite spec_eval%in; apply Pf%in." size size
-    else 
+    else
       pp "     intros m y; rewrite spec_extend%in%i; rewrite spec_eval%in; apply Pf%in." i size size size;
   done;
   pp "    intros n x y; case y; clear y.";
   for i = 0 to size do
     if i == size then
       pp "     intros y; rewrite spec_eval%in; apply Pfn%i." size size
-    else 
+    else
       pp "      intros y; rewrite spec_extend%in%i; rewrite spec_eval%in; apply Pfn%i." i size size size;
   done;
   pp "  intros m y; apply Pfnm.";
@@ -820,8 +820,8 @@ let _ =
       pr "    | %s%i wy => f%in %i wx wy" c j i (j - i - 1);
     done;
     if i == size then
-      pr "    | %sn m wy => f%in m wx wy" c size 
-    else 
+      pr "    | %sn m wy => f%in m wx wy" c size
+    else
       pr "    | %sn m wy => f%in m (extend%i %i wx) wy" c size i (size - i - 1);
     pr "    end";
   done;
@@ -832,8 +832,8 @@ let _ =
     if i == 0 then
       pr "      if w0_eq0 wy then ft0 x else";
     if i == size then
-      pr "      fn%i n wx wy" size 
-    else 
+      pr "      fn%i n wx wy" size
+    else
       pr "      fn%i n wx (extend%i %i wy)" size i (size - i - 1);
   done;
   pr "    | %sn m wy => fnm n m wx wy" c;
@@ -869,7 +869,7 @@ let _ =
     done;
     if i == size then
       pp "     intros m y; rewrite spec_eval%in; apply Pf%in." size size
-    else 
+    else
       pp "     intros m y; rewrite spec_extend%in%i; rewrite spec_eval%in; apply Pf%in." i size size size;
   done;
   pp "    intros n x y; case y; clear y.";
@@ -883,7 +883,7 @@ let _ =
       end;
     if i == size then
       pp "     rewrite spec_eval%in; apply Pfn%i." size size
-    else 
+    else
       pp "      rewrite spec_extend%in%i; rewrite spec_eval%in; apply Pfn%i." i size size size;
   done;
   pp "  intros m y; apply Pfnm.";
@@ -902,20 +902,20 @@ let _ =
   pr " (***************************************************************)";
   pr "";
 
-  pr " Definition reduce_0 (x:w) := %s0 x." c; 
+  pr " Definition reduce_0 (x:w) := %s0 x." c;
   pr " Definition reduce_1 :=";
   pr "  Eval lazy beta iota delta[reduce_n1] in";
   pr "   reduce_n1 _ _ zero w0_eq0 %s0 %s1." c c;
   for i = 2 to size do
     pr " Definition reduce_%i :=" i;
     pr "  Eval lazy beta iota delta[reduce_n1] in";
-    pr "   reduce_n1 _ _ zero w%i_eq0 reduce_%i %s%i." 
+    pr "   reduce_n1 _ _ zero w%i_eq0 reduce_%i %s%i."
       (i-1) (i-1)  c i
   done;
   pr " Definition reduce_%i :=" (size+1);
   pr "  Eval lazy beta iota delta[reduce_n1] in";
-  pr "   reduce_n1 _ _ zero w%i_eq0 reduce_%i (%sn 0)." 
-    size size c; 
+  pr "   reduce_n1 _ _ zero w%i_eq0 reduce_%i (%sn 0)."
+    size size c;
 
   pr " Definition reduce_n n := ";
   pr "  Eval lazy beta iota delta[reduce_n] in";
@@ -940,7 +940,7 @@ let _ =
     pp " intros x1 y1.";
     pp " generalize (spec_w%i_eq0 x1); " (i - 1);
     pp "   case w%i_eq0; intros H1; auto." (i - 1);
-    if i <> 1 then 
+    if i <> 1 then
       pp " rewrite spec_reduce_%i." (i - 1);
     pp " unfold to_Z; rewrite znz_to_Z_%i." i;
     pp " unfold to_Z in H1; rewrite H1; auto.";
@@ -983,19 +983,19 @@ let _ =
   for i = 0 to size-1 do
     pr "  | %s%i wx =>" c i;
     pr "    match w%i_succ_c wx with" i;
-    pr "    | C0 r => %s%i r" c i; 
+    pr "    | C0 r => %s%i r" c i;
     pr "    | C1 r => %s%i (WW one%i r)" c (i+1) i;
     pr "    end";
   done;
   pr "  | %s%i wx =>" c size;
   pr "    match w%i_succ_c wx with" size;
-  pr "    | C0 r => %s%i r" c size; 
+  pr "    | C0 r => %s%i r" c size;
   pr "    | C1 r => %sn 0 (WW one%i r)" c size ;
   pr "    end";
   pr "  | %sn n wx =>" c;
   pr "    let op := make_op n in";
   pr "    match op.(znz_succ_c) wx with";
-  pr "    | C0 r => %sn n r" c; 
+  pr "    | C0 r => %sn n r" c;
   pr "    | C1 r => %sn (S n) (WW op.(znz_1) r)" c;
   pr "    end";
   pr "  end.";
@@ -1033,7 +1033,7 @@ let _ =
   pr "";
 
   for i = 0 to size do
-    pr " Definition w%i_add_c := znz_add_c w%i_op." i i; 
+    pr " Definition w%i_add_c := znz_add_c w%i_op." i i;
     pr " Definition w%i_add x y :=" i;
     pr "  match w%i_add_c x y with" i;
     pr "  | C0 r => %s%i r" c i;
@@ -1057,7 +1057,7 @@ let _ =
     pp " Proof.";
     pp " intros n m; unfold to_Z, w%i_add, w%i_add_c." i i;
     pp "  generalize (spec_add_c w%i_spec n m); case znz_add_c; auto." i;
-    pp " intros ww H; rewrite <- H."; 
+    pp " intros ww H; rewrite <- H.";
     pp "    rewrite znz_to_Z_%i; unfold interp_carry;" (i + 1);
     pp "    apply f_equal2 with (f := Zplus); auto;";
     pp "    apply f_equal2 with (f := Zmult); auto;";
@@ -1070,7 +1070,7 @@ let _ =
   pp " Proof.";
   pp " intros k n m; unfold to_Z, addn.";
   pp "  generalize (spec_add_c (wn_spec k) n m); case znz_add_c; auto.";
-  pp " intros ww H; rewrite <- H."; 
+  pp " intros ww H; rewrite <- H.";
   pp " rewrite (znz_to_Z_n k); unfold interp_carry;";
   pp "        apply f_equal2 with (f := Zplus); auto;";
   pp "        apply f_equal2 with (f := Zmult); auto;";
@@ -1116,14 +1116,14 @@ let _ =
   for i = 0 to size do
     pr "  | %s%i wx =>" c i;
     pr "    match w%i_pred_c wx with" i;
-    pr "    | C0 r => reduce_%i r" i; 
+    pr "    | C0 r => reduce_%i r" i;
     pr "    | C1 r => zero";
     pr "    end";
   done;
   pr "  | %sn n wx =>" c;
   pr "    let op := make_op n in";
   pr "    match op.(znz_pred_c) wx with";
-  pr "    | C0 r => reduce_n n r"; 
+  pr "    | C0 r => reduce_n n r";
   pr "    | C1 r => zero";
   pr "    end";
   pr "  end.";
@@ -1153,7 +1153,7 @@ let _ =
   pp " unfold to_Z in H1; auto with zarith.";
   pp " Qed.";
   pp " ";
-  
+
   pp " Let spec_pred0: forall x, [x] = 0 -> [pred x] = 0.";
   pp " Proof.";
   pp " intros x; case x; unfold pred.";
@@ -1187,7 +1187,7 @@ let _ =
   done;
   pr "";
 
-  for i = 0 to size do 
+  for i = 0 to size do
     pr " Definition w%i_sub x y :=" i;
     pr "  match w%i_sub_c x y with" i;
     pr "  | C0 r => reduce_%i r" i;
@@ -1209,7 +1209,7 @@ let _ =
     pp " Proof.";
     pp " intros n m; unfold w%i_sub, w%i_sub_c." i i;
     pp "  generalize (spec_sub_c w%i_spec n m); case znz_sub_c; " i;
-    if i == 0 then 
+    if i == 0 then
       pp "    intros x; auto."
     else
       pp "   intros x; try rewrite spec_reduce_%i; auto." i;
@@ -1219,7 +1219,7 @@ let _ =
     pp " Qed.";
     pp "";
   done;
-  
+
   pp " Let spec_wn_sub: forall n x y, [%sn n y] <= [%sn n x] -> [subn n x y] = [%sn n x] - [%sn n y]." c c c c;
   pp " Proof.";
   pp " intros k n m; unfold subn.";
@@ -1299,7 +1299,7 @@ let _ =
     pr " Definition comparen_%i :=" i;
     pr "  compare_mn_1 w%i w%i %s compare_%i (compare_%i %s) compare_%i." i i (pz i) i i (pz i) i
   done;
-  pr ""; 
+  pr "";
 
   pr " Definition comparenm n m wx wy :=";
   pr "    let mn := Max.max n m in";
@@ -1337,7 +1337,7 @@ let _ =
     pp "  unfold compare_%i, to_Z; exact (spec_compare w%i_spec)." i i;
     pp "  Qed.";
     pp "";
-    
+
     pp "  Let spec_comparen_%i:" i;
     pp "  forall (n : nat) (x : word w%i n) (y : w%i)," i i;
     pp "  match comparen_%i n x y with" i;
@@ -1387,12 +1387,12 @@ let _ =
     pp "      (fun n => comparen_%i (S n)) _ _ _" i;
   done;
   pp "      comparenm _).";
-  
+
   for i = 0 to size - 1 do
     pp "  exact spec_compare_%i." i;
     pp "  intros n x y H;apply spec_opp_compare; apply spec_comparen_%i." i;
     pp "  intros n x y H; exact (spec_comparen_%i (S n) x y)." i;
-  done; 
+  done;
   pp "  exact spec_compare_%i." size;
   pp "  intros n x y;apply spec_opp_compare; apply spec_comparen_%i." size;
   pp "  intros n; exact (spec_comparen_%i (S n))." size;
@@ -1461,7 +1461,7 @@ let _ =
     pr "  match n return word w%i (S n) -> t_ with" i;
     for j = 0 to size - i do
       if (i + j) == size then
-        begin 
+        begin
           pr "  | %i%s => fun x => %sn 0 x" j "%nat" c;
           pr "  | %i%s => fun x => %sn 1 x" (j + 1) "%nat" c
         end
@@ -1471,7 +1471,7 @@ let _ =
     pr   "  | _   => fun _ => N0 w_0";
     pr "  end.";
     pr "";
-  done; 
+  done;
 
 
   for i = 0 to size - 1 do
@@ -1486,7 +1486,7 @@ let _ =
     pp " repeat rewrite inj_S; unfold Zsucc; auto with zarith.";
     pp " Qed.";
     pp "";
-  done; 
+  done;
 
 
   for i = 0 to size do
@@ -1497,8 +1497,8 @@ let _ =
         pr " if w%i_eq0 w then %sn n r" i c;
         pr " else %sn (S n) (WW (extend%i n w) r)." c i;
       end
-    else 
-      begin 
+    else
+      begin
         pr " if w%i_eq0 w then to_Z%i n r" i i;
         pr " else to_Z%i (S n) (WW (extend%i n w) r)." i i;
       end;
@@ -1556,7 +1556,7 @@ let _ =
     pp " Qed.";
     pp "";
   done;
-  
+
   pp "  Lemma nmake_op_WW: forall ww ww1 n x y,";
   pp "    znz_to_Z (nmake_op ww ww1 (S n)) (WW x y) =";
   pp "    znz_to_Z (nmake_op ww ww1 n) x * base (znz_digits (nmake_op ww ww1 n)) +";
@@ -1564,7 +1564,7 @@ let _ =
   pp "    auto.";
   pp "  Qed.";
   pp "";
-  
+
   for i = 0 to size do
     pp "  Lemma extend%in_spec: forall n x1," i;
     pp "  znz_to_Z (nmake_op _ w%i_op (S n)) (extend%i n x1) = " i i;
@@ -1573,12 +1573,12 @@ let _ =
     pp "    intros n1 x2; rewrite nmake_double.";
     pp "    unfold extend%i." i;
     pp "    rewrite DoubleBase.spec_extend; auto.";
-    if i == 0 then 
+    if i == 0 then
       pp "    intros l; simpl; unfold w_0; rewrite (spec_0 w0_spec); ring.";
     pp "  Qed.";
     pp "";
   done;
-  
+
   pp "  Lemma spec_muln:";
   pp "    forall n (x: word _ (S n)) y,";
   pp "     [%sn (S n) (znz_mul_c (make_op n) x y)] = [%sn n x] * [%sn n y]." c c c;
@@ -1614,7 +1614,7 @@ let _ =
     pp "    generalize (spec_w%i_eq0 x1); case w%i_eq0; intros HH." i i;
     pp "    unfold to_Z in HH; rewrite HH.";
     if i == size then
-      begin 
+      begin
         pp "    rewrite spec_eval%in; unfold eval%in, nmake_op%i; auto." i i i;
         pp "    rewrite spec_eval%in; unfold eval%in, nmake_op%i." i i i
       end
@@ -1708,7 +1708,7 @@ let _ =
   pr " (*                           Power                             *)";
   pr " (*                                                             *)";
   pr " (***************************************************************)";
-  pr ""; 
+  pr "";
 
   pr " Fixpoint power_pos (x:%s) (p:positive) {struct p} : %s :=" t t;
   pr "  match p with";
@@ -1719,7 +1719,7 @@ let _ =
   pr "";
 
   pr " Theorem spec_power_pos: forall x n, [power_pos x n] = [x] ^ Zpos n.";
-  pa " Admitted.";  
+  pa " Admitted.";
   pp " Proof.";
   pp " intros x n; generalize x; elim n; clear n x; simpl power_pos.";
   pp " intros; rewrite spec_mul; rewrite spec_square; rewrite H.";
@@ -1775,7 +1775,7 @@ let _ =
   pr " (*                           Division                          *)";
   pr " (*                                                             *)";
   pr " (***************************************************************)";
-  pr ""; 
+  pr "";
 
   for i = 0 to size do
     pr " Definition w%i_div_gt := w%i_op.(znz_div_gt)." i i
@@ -1844,7 +1844,7 @@ let _ =
 
   pr " Definition div_gt := Eval lazy beta delta [iter] in";
   pr "   (iter _ ";
-  for i = 0 to size do 
+  for i = 0 to size do
     pr "      div_gt%i" i;
     pr "      (fun n x y => div_gt%i x (DoubleBase.get_low %s (S n) y))" i (pz i);
     pr "      w%i_divn1" i;
@@ -1862,10 +1862,10 @@ let _ =
   pp "   forall x y, [x] > [y] -> 0 < [y] ->";
   pp "      let (q,r) := div_gt x y in";
   pp "      [x] = [q] * [y] + [r] /\\ 0 <= [r] < [y]).";
-  pp "  refine (spec_iter (t_*t_) (fun x y res => x > y -> 0 < y ->";  
+  pp "  refine (spec_iter (t_*t_) (fun x y res => x > y -> 0 < y ->";
   pp "      let (q,r) := res in";
   pp "      x = [q] * y + [r] /\\ 0 <= [r] < y)";
-  for i = 0 to size do 
+  for i = 0 to size do
     pp "      div_gt%i" i;
     pp "      (fun n x y => div_gt%i x (DoubleBase.get_low %s (S n) y))" i (pz i);
     pp "      w%i_divn1 _ _ _" i;
@@ -1883,7 +1883,7 @@ let _ =
     pp "                (DoubleBase.get_low %s (S n) y))." (pz i);
     pp0 "    ";
     for j = 0 to i do
-      pp0 "unfold w%i; " (i-j); 
+      pp0 "unfold w%i; " (i-j);
     done;
     pp "case znz_div_gt.";
     pp "    intros xx yy H4; repeat rewrite spec_reduce_%i." i;
@@ -1897,7 +1897,7 @@ let _ =
     pp "     (spec_divn1 w%i w%i_op w%i_spec (S n) x y H3)." i i i;
     pp0 "    unfold w%i_divn1; " i;
     for j = 0 to i do
-      pp0 "unfold w%i; " (i-j); 
+      pp0 "unfold w%i; " (i-j);
     done;
     pp "case double_divn1.";
     pp "    intros xx yy H4.";
@@ -1990,7 +1990,7 @@ let _ =
   pr " (*                           Modulo                            *)";
   pr " (*                                                             *)";
   pr " (***************************************************************)";
-  pr ""; 
+  pr "";
 
   for i = 0 to size do
     pr " Definition w%i_mod_gt := w%i_op.(znz_mod_gt)." i i
@@ -2063,7 +2063,7 @@ let _ =
     pp " rewrite <- (spec_get_end%i (S n) y x) in H3; auto with zarith." i;
     if i == size then
       pp " intros n x y H2 H3; rewrite spec_reduce_%i." i
-    else 
+    else
       pp " intros n x y H1 H2 H3; rewrite spec_reduce_%i." i;
     pp " unfold w%i_modn1, to_Z; rewrite spec_double_eval%in." i i;
     pp " apply (spec_modn1 _ _ w%i_spec); auto." i;
@@ -2110,7 +2110,7 @@ let _ =
   pr " (*                           Gcd                               *)";
   pr " (*                                                             *)";
   pr " (***************************************************************)";
-  pr ""; 
+  pr "";
 
   pr " Definition digits x :=";
   pr "  match x with";
@@ -2423,7 +2423,7 @@ let _ =
   pr " (*                          Shift                              *)";
   pr " (*                                                             *)";
   pr " (***************************************************************)";
-  pr ""; 
+  pr "";
 
   (* Head0 *)
   pr " Definition head0 w := match w with";
@@ -2513,7 +2513,7 @@ let _ =
   pr " Definition %sdigits x :=" c;
   pr "  match x with";
   pr "  | %s0 _ => %s0 w0_op.(znz_zdigits)" c c;
-  for i = 1 to size do 
+  for i = 1 to size do
     pr "  | %s%i _ => reduce_%i w%i_op.(znz_zdigits)" c i i i;
   done;
   pr "  | %sn n _ => reduce_n n (make_op n).(znz_zdigits)" c;
@@ -2644,7 +2644,7 @@ let _ =
         pp "       apply F4 with (3:=(wn_spec m))(4:=wn_spec m)(5:=w%i_spec); auto with zarith." size;
         pp "       try (apply sym_equal; exact (spec_extend%in m x))." size;
       end
-    else 
+    else
       begin
         pp "     intros m y; unfold shiftrn, Ndigits.";
         pp "       repeat rewrite spec_reduce_n; unfold to_Z; intros H1.";
@@ -2857,7 +2857,7 @@ let _ =
         pp "       apply F4 with (3:=(wn_spec m))(4:=wn_spec m)(5:=w%i_spec); auto with zarith." size;
         pp "       try (apply sym_equal; exact (spec_extend%in m x))." size;
       end
-    else 
+    else
       begin
         pp "     intros m y; unfold shiftln, head0.";
         pp "       repeat rewrite spec_reduce_n; unfold to_Z; intros H1.";
@@ -3030,7 +3030,7 @@ let _ =
   pr "      (forall x, 2 ^ (Zpos p + 1) <= [head0 x]->";
   pr "         [cont n x] = [x] * 2 ^ [n]) ->";
   pr "      [safe_shiftl_aux_body cont n x] = [x] * 2 ^ [n].";
-  pa " Admitted.";  
+  pa " Admitted.";
   pp " Proof.";
   pp " intros n p x cont H1 H2; unfold safe_shiftl_aux_body.";
   pp " generalize (spec_compare n (head0 x)); case compare; intros H.";
diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v
index c3fdd1bf4..d42db97d5 100644
--- a/theories/Numbers/Natural/BigN/Nbasic.v
+++ b/theories/Numbers/Natural/BigN/Nbasic.v
@@ -21,7 +21,7 @@ Require Import DoubleCyclic.
 (* To compute the necessary height *)
 
 Fixpoint plength (p: positive) : positive :=
-  match p with 
+  match p with
     xH => xH
   | xO p1 => Psucc (plength p1)
   | xI p1 => Psucc (plength p1)
@@ -34,10 +34,10 @@ rewrite Zpower_exp; auto with zarith.
 rewrite Zpos_succ_morphism; unfold Zsucc; auto with zarith.
 intros p; elim p; simpl plength; auto.
 intros p1 Hp1; rewrite F; repeat rewrite Zpos_xI.
-assert (tmp: (forall p, 2 * p = p + p)%Z); 
+assert (tmp: (forall p, 2 * p = p + p)%Z);
   try repeat rewrite tmp; auto with zarith.
 intros p1 Hp1; rewrite F; rewrite (Zpos_xO p1).
-assert (tmp: (forall p, 2 * p = p + p)%Z); 
+assert (tmp: (forall p, 2 * p = p + p)%Z);
   try repeat rewrite tmp; auto with zarith.
 rewrite Zpower_1_r; auto with zarith.
 Qed.
@@ -73,7 +73,7 @@ case (Z_mod_lt (Zpos p) (Zpos q) H1); auto with zarith.
 intros q1 H2.
 replace (Zpos p - Zpos q * Zpos q1) with (Zpos p mod Zpos q).
   2: pattern (Zpos p) at 2; rewrite H2; auto with zarith.
-generalize H2 (Z_mod_lt (Zpos p) (Zpos q) H1); clear H2; 
+generalize H2 (Z_mod_lt (Zpos p) (Zpos q) H1); clear H2;
   case Zmod.
   intros HH _; rewrite HH; auto with zarith.
   intros r1 HH (_,HH1); rewrite HH; rewrite Zpos_succ_morphism.
@@ -121,9 +121,9 @@ Definition zn2z_word_comm : forall w n, zn2z (word w n) = word (zn2z w) n.
 Defined.
 
 Fixpoint extend (n:nat) {struct n} : forall w:Type, zn2z w -> word w (S n) :=
- match n return forall w:Type, zn2z w -> word w (S n) with 
+ match n return forall w:Type, zn2z w -> word w (S n) with
  | O => fun w x => x
- | S m => 
+ | S m =>
    let aux := extend m in
    fun w x => WW W0 (aux w x)
  end.
@@ -169,7 +169,7 @@ Fixpoint diff_l (m n : nat) {struct m} : fst (diff m n) + n = max m n :=
       | S n1 =>
           let v := fst (diff m1 n1) + n1 in
           let v1 := fst (diff m1 n1) + S n1 in
-          eq_ind v (fun n => v1 = S n) 
+          eq_ind v (fun n => v1 = S n)
             (eq_ind v1 (fun n => v1 = n) (refl_equal v1) (S v) (plusnS _ _))
             _ (diff_l _ _)
       end
@@ -182,7 +182,7 @@ Fixpoint diff_r (m n: nat) {struct m}: snd (diff m n) + m = max m n :=
       | 0 => refl_equal _
       | S _ => plusn0 _
       end
-  | S m => 
+  | S m =>
       match n return (snd (diff (S m) n) + S m = max (S m) n) with
       | 0 => refl_equal (snd (diff (S m) 0) + S m)
       | S n1 =>
@@ -253,9 +253,9 @@ Section ReduceRec.
     | WW xh xl =>
       match xh with
       | W0 => @reduce_n m xl
-      | _ => @c (S m) x 
+      | _ => @c (S m) x
       end
-    end	
+    end
   end.
 
 End ReduceRec.
@@ -276,14 +276,14 @@ Section CompareRec.
  Variable compare_m : wm -> w -> comparison.
 
  Fixpoint compare0_mn (n:nat) : word wm n -> comparison :=
-  match n return word wm n -> comparison with 
-  | O => compare0_m 
+  match n return word wm n -> comparison with
+  | O => compare0_m
   | S m => fun x =>
     match x with
     | W0 => Eq
-    | WW xh xl => 
+    | WW xh xl =>
       match compare0_mn m xh with
-      | Eq => compare0_mn m xl 
+      | Eq => compare0_mn m xl
       | r  => Lt
       end
     end
@@ -296,7 +296,7 @@ Section CompareRec.
  Variable spec_compare0_m: forall x,
     match compare0_m x with
       Eq => w_to_Z w_0 = wm_to_Z x
-    | Lt => w_to_Z w_0 < wm_to_Z x 
+    | Lt => w_to_Z w_0 < wm_to_Z x
     | Gt => w_to_Z w_0 > wm_to_Z x
     end.
  Variable wm_to_Z_pos: forall x, 0 <= wm_to_Z x < base wm_base.
@@ -341,14 +341,14 @@ Section CompareRec.
   Qed.
 
  Fixpoint compare_mn_1 (n:nat) : word wm n -> w -> comparison :=
-  match n return word wm n -> w -> comparison with 
-  | O => compare_m 
-  | S m => fun x y => 
+  match n return word wm n -> w -> comparison with
+  | O => compare_m
+  | S m => fun x y =>
     match x with
     | W0 => compare w_0 y
-    | WW xh xl => 
+    | WW xh xl =>
       match compare0_mn m xh with
-      | Eq => compare_mn_1 m xl y 
+      | Eq => compare_mn_1 m xl y
       | r  => Gt
       end
     end
@@ -366,7 +366,7 @@ Section CompareRec.
    | Lt => wm_to_Z x < w_to_Z y
    | Gt => wm_to_Z x > w_to_Z y
    end.
- Variable wm_base_lt: forall x, 
+ Variable wm_base_lt: forall x,
    0 <= w_to_Z x < base (wm_base).
 
  Let double_wB_lt: forall n x,
@@ -385,7 +385,7 @@ Section CompareRec.
  unfold Zpower_pos; simpl; ring.
  Qed.
 
- 
+
  Lemma spec_compare_mn_1: forall n x y,
    match compare_mn_1 n x y with
      Eq => double_to_Z n x = w_to_Z y
@@ -434,7 +434,7 @@ Section AddS.
                 | C1 z => match incr hy with
                             C0 z1 => C0 (WW z1 z)
                           | C1 z1 => C1 (WW z1 z)
-                          end  
+                          end
                  end
    end.
 
@@ -458,12 +458,12 @@ End AddS.
 
  Fixpoint length_pos x :=
   match x with xH => O | xO x1 => S (length_pos x1) | xI x1 => S (length_pos x1) end.
- 
+
  Theorem length_pos_lt: forall x y,
    (length_pos x < length_pos y)%nat -> Zpos x < Zpos y.
  Proof.
  intros x; elim x; clear x; [intros x1 Hrec | intros x1 Hrec | idtac];
-   intros y; case y; clear y; intros y1 H || intros H; simpl length_pos; 
+   intros y; case y; clear y; intros y1 H || intros H; simpl length_pos;
    try (rewrite (Zpos_xI x1) || rewrite (Zpos_xO x1));
    try (rewrite (Zpos_xI y1) || rewrite (Zpos_xO y1));
    try (inversion H; fail);
@@ -492,20 +492,20 @@ End AddS.
  Qed.
 
  Theorem make_zop: forall w (x: znz_op w),
-  znz_to_Z (mk_zn2z_op x) = 
-    fun z => match z with 
+  znz_to_Z (mk_zn2z_op x) =
+    fun z => match z with
                 W0 => 0
-             | WW xh xl => znz_to_Z x xh * base (znz_digits x) 
+             | WW xh xl => znz_to_Z x xh * base (znz_digits x)
                                 + znz_to_Z x xl
              end.
  intros ww x; auto.
  Qed.
 
  Theorem make_kzop: forall w (x: znz_op w),
-  znz_to_Z (mk_zn2z_op_karatsuba x) = 
-    fun z => match z with 
+  znz_to_Z (mk_zn2z_op_karatsuba x) =
+    fun z => match z with
                 W0 => 0
-             | WW xh xl => znz_to_Z x xh * base (znz_digits x) 
+             | WW xh xl => znz_to_Z x xh * base (znz_digits x)
                                 + znz_to_Z x xl
              end.
  intros ww x; auto.