Merge pull request #8 from clarus/master

Bug fixes for conversions from integers to strings.

Author: gmalecha

theories/Data/Char.v

@@ -64,7 +64,7 @@ Definition digit2ascii (n:nat) : Ascii.ascii :=
     | 7 => "7"
     | 8 => "8"
     | 9 => "9"
-    | n => ascii_of_nat (n - 9 + nat_of_ascii "A")
+    | n => ascii_of_nat (n - 10 + nat_of_ascii "A")
   end%char.
 
 Definition chr_newline : ascii :=

theories/Data/String.v

@@ -90,7 +90,7 @@ Section Program_Scope.
       | true => fun _ => String (digit2ascii n) EmptyString
       | false => fun pf =>
         let m := NPeano.div n mod in
-        append (nat2string m) (String (digit2ascii (n - 10 * m)) EmptyString)
+        append (nat2string m) (String (digit2ascii (n - mod * m)) EmptyString)
     end eq_refl.
   Next Obligation.
     eapply NPeano.Nat.div_lt; auto.