summaryrefslogtreecommitdiff
path: root/backend/Bounds.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/Bounds.v')
-rw-r--r--backend/Bounds.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/backend/Bounds.v b/backend/Bounds.v
index 23fa3b5..ef78b2e 100644
--- a/backend/Bounds.v
+++ b/backend/Bounds.v
@@ -13,7 +13,6 @@
(** Computation of resource bounds for Linear code. *)
Require Import Coqlib.
-Require Import Maps.
Require Import AST.
Require Import Op.
Require Import Locations.