Decimal: prove numeral notation for Q

Fill in the proofs, adding a few neessary lemmas along the way.

1 files changed, 7 insertions, 3 deletions

diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v
index 2a84456500..5eae5567d7 100644
--- a/theories/Init/Decimal.v
+++ b/theories/Init/Decimal.v
@@ -16,7 +16,7 @@
     We represent numbers in base 10 as lists of decimal digits,
     in big-endian order (most significant digit comes first). *)
 
-Require Import Datatypes.
+Require Import Datatypes Specif.
 
 (** Unsigned integers are just lists of digits.
     For instance, ten is (D1 (D0 Nil)) *)
@@ -53,6 +53,10 @@ Variant decimal :=
  | Decimal (i:int) (f:uint)
  | DecimalExp (i:int) (f:uint) (e:int).
 
+Scheme Equality for uint.
+Scheme Equality for int.
+Scheme Equality for decimal.
+
 Declare Scope dec_uint_scope.
 Delimit Scope dec_uint_scope with uint.
 Bind Scope dec_uint_scope with uint.
@@ -172,8 +176,8 @@ Fixpoint del_head n d :=
 
 Definition del_head_int n d :=
   match d with
-  | Pos d => Pos (del_head n d)
-  | Neg d => Neg (del_head n d)
+  | Pos d => del_head n d
+  | Neg d => del_head n d
   end.
 
 (** [del_tail n d] removes [n] digits at end of [d]