From fb56c4eb9cb4afe4365c05e0cc6ba2643064ee6b Mon Sep 17 00:00:00 2001
From: Yishuai Li
Date: Mon, 29 Oct 2018 13:21:08 -0400
Subject: NArith: implicit length argument for Bv2N

---
 CHANGES.md                | 1 +
 theories/NArith/Ndigits.v | 6 ++++--
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/CHANGES.md b/CHANGES.md
index 363513e4f7..21d9c41073 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -28,6 +28,7 @@ Standard Library
 
 - Added lemmas about monotonicity of `N.double` and `N.succ_double`, and about
   the upper bound of number represented by a vector.
+  Allowed implicit vector length argument in `Ndigits.Bv2N`.
 
 Changes from 8.8.2 to 8.9+beta1
 ===============================
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v
index 0f585baa4a..fb1cef1ddd 100644
--- a/theories/NArith/Ndigits.v
+++ b/theories/NArith/Ndigits.v
@@ -546,8 +546,10 @@ Fixpoint Bv2N (n:nat)(bv:Bvector n) : N :=
     | Vector.cons _ true n bv => N.succ_double (Bv2N n bv)
   end.
 
+Arguments Bv2N {n} bv, n bv.
+
 Definition ByteV2N {n : nat} : ByteVector n -> N :=
-  Bv2N (n * 8) ∘ to_Bvector.
+  Bv2N ∘ to_Bvector.
 
 Lemma Bv2N_N2Bv : forall n, Bv2N _ (N2Bv n) = n.
 Proof.
@@ -584,7 +586,7 @@ destruct a ; compute ; split ; intros x ; now inversion x.
 Qed.
 
 Lemma Bv2N_upper_bound (n : nat) (bv : Bvector n) :
-    (Bv2N n bv < N.shiftl_nat 1 n)%N.
+    (Bv2N bv < N.shiftl_nat 1 n)%N.
 Proof with simpl; auto.
   induction bv...
   - constructor.
-- 
cgit v1.2.3