From e2683e1e653a1b6872a886f4b99218e2803f7a74 Mon Sep 17 00:00:00 2001
From: vblot <24938579+vblot@users.noreply.github.com>
Date: Wed, 7 Jul 2021 08:55:25 +0200
Subject: use native integers (#96)

---
 src/bva/BVList.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/bva/BVList.v')

diff --git a/src/bva/BVList.v b/src/bva/BVList.v
index 91a110d..f0ba8ef 100644
--- a/src/bva/BVList.v
+++ b/src/bva/BVList.v
@@ -435,7 +435,7 @@ Fixpoint beq_listP (l m : list bool) {struct l} :=
 Lemma bv_mk_eq l1 l2 : bv_eq l1 l2 = beq_list l1 l2.
 Proof.
   unfold bv_eq, size, bits.
-  case_eq (Nat_eqb (length l1) (length l2)); intro Heq.
+  case_eq (Nat.eqb (length l1) (length l2)); intro Heq.
   - now rewrite (EqNat.beq_nat_true _ _ Heq), N.eqb_refl.
   - replace (N.of_nat (length l1) =? N.of_nat (length l2)) with false.
     * revert l2 Heq. induction l1 as [ |b1 l1 IHl1]; intros [ |b2 l2]; simpl in *; auto.
-- 
cgit