aboutsummaryrefslogtreecommitdiffstats
path: root/src/bva/BVList.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/bva/BVList.v')
-rw-r--r--src/bva/BVList.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/bva/BVList.v b/src/bva/BVList.v
index 48befd6..a53970b 100644
--- a/src/bva/BVList.v
+++ b/src/bva/BVList.v
@@ -10,7 +10,7 @@
(**************************************************************************)
-Require Import List Bool NArith Psatz Int63 Nnat.
+Require Import List Bool NArith Psatz Int63 Nnat ZArith.
Require Import Misc.
Import ListNotations.
Local Open Scope list_scope.