aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/ValueVal.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/hls/ValueVal.v')
-rw-r--r--src/hls/ValueVal.v2
1 files changed, 0 insertions, 2 deletions
diff --git a/src/hls/ValueVal.v b/src/hls/ValueVal.v
index b882dc6..96e0b1c 100644
--- a/src/hls/ValueVal.v
+++ b/src/hls/ValueVal.v
@@ -17,8 +17,6 @@
*)
(* begin hide *)
-From bbv Require Import Word.
-From bbv Require HexNotation WordScope.
From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia.
From compcert Require Export lib.Integers common.Values.
From vericert Require Import Vericertlib.