summaryrefslogtreecommitdiff
path: root/backend/Reloadtyping.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/Reloadtyping.v')
-rw-r--r--backend/Reloadtyping.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v
index eba5ad6..99c89ab 100644
--- a/backend/Reloadtyping.v
+++ b/backend/Reloadtyping.v
@@ -14,7 +14,6 @@
correctness of computation of stack bounds for Linear. *)
Require Import Coqlib.
-Require Import Maps.
Require Import AST.
Require Import Op.
Require Import Locations.