1 files changed, 17 insertions, 21 deletions
diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v
index 72d35827e..8f2648269 100644
--- a/theories/Init/Nat.v
+++ b/theories/Init/Nat.v
@@ -136,25 +136,21 @@ where "n ^ m" := (pow n m) : nat_scope.
 
 (** ** Tail-recursive versions of [add] and [mul] *)
 
-Module Tail.
-
-Fixpoint add n m :=
+Fixpoint tail_add n m :=
   match n with
     | O => m
-    | S n => add n (S m)
+    | S n => tail_add n (S m)
   end.
 
-(** [addmul r n m] is [r + n * m]. *)
+(** [tail_addmul r n m] is [r + n * m]. *)
 
-Fixpoint addmul r n m :=
+Fixpoint tail_addmul r n m :=
   match n with
     | O => r
-    | S n => addmul (add m r) n m
+    | S n => tail_addmul (tail_add m r) n m
   end.
 
-Definition mul n m := addmul 0 n m.
-
-End Tail.
+Definition tail_mul n m := tail_addmul 0 n m.
 
 (** ** Conversion with a decimal representation for printing/parsing *)
 
@@ -163,16 +159,16 @@ Local Notation ten := (S (S (S (S (S (S (S (S (S (S O)))))))))).
 Fixpoint of_uint_acc (d:Decimal.uint)(acc:nat) :=
   match d with
   | Decimal.Nil => acc
-  | Decimal.D0 d => of_uint_acc d (Tail.mul ten acc)
-  | Decimal.D1 d => of_uint_acc d (S (Tail.mul ten acc))
-  | Decimal.D2 d => of_uint_acc d (S (S (Tail.mul ten acc)))
-  | Decimal.D3 d => of_uint_acc d (S (S (S (Tail.mul ten acc))))
-  | Decimal.D4 d => of_uint_acc d (S (S (S (S (Tail.mul ten acc)))))
-  | Decimal.D5 d => of_uint_acc d (S (S (S (S (S (Tail.mul ten acc))))))
-  | Decimal.D6 d => of_uint_acc d (S (S (S (S (S (S (Tail.mul ten acc)))))))
-  | Decimal.D7 d => of_uint_acc d (S (S (S (S (S (S (S (Tail.mul ten acc))))))))
-  | Decimal.D8 d => of_uint_acc d (S (S (S (S (S (S (S (S (Tail.mul ten acc)))))))))
-  | Decimal.D9 d => of_uint_acc d (S (S (S (S (S (S (S (S (S (Tail.mul ten acc))))))))))
+  | Decimal.D0 d => of_uint_acc d (tail_mul ten acc)
+  | Decimal.D1 d => of_uint_acc d (S (tail_mul ten acc))
+  | Decimal.D2 d => of_uint_acc d (S (S (tail_mul ten acc)))
+  | Decimal.D3 d => of_uint_acc d (S (S (S (tail_mul ten acc))))
+  | Decimal.D4 d => of_uint_acc d (S (S (S (S (tail_mul ten acc)))))
+  | Decimal.D5 d => of_uint_acc d (S (S (S (S (S (tail_mul ten acc))))))
+  | Decimal.D6 d => of_uint_acc d (S (S (S (S (S (S (tail_mul ten acc)))))))
+  | Decimal.D7 d => of_uint_acc d (S (S (S (S (S (S (S (tail_mul ten acc))))))))
+  | Decimal.D8 d => of_uint_acc d (S (S (S (S (S (S (S (S (tail_mul ten acc)))))))))
+  | Decimal.D9 d => of_uint_acc d (S (S (S (S (S (S (S (S (S (tail_mul ten acc))))))))))
   end.
 
 Definition of_uint (d:Decimal.uint) := of_uint_acc d O.
@@ -184,7 +180,7 @@ Fixpoint to_little_uint n acc :=
   end.
 
 Definition to_uint n :=
-  Decimal.rev (to_little_uint n Decimal.zero) Decimal.Nil.
+  Decimal.rev (to_little_uint n Decimal.zero).
 
 Definition of_int (d:Decimal.int) : option nat :=
   match Decimal.norm d with