summaryrefslogtreecommitdiff
path: root/backend/Tunnelingtyping.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/Tunnelingtyping.v')
-rw-r--r--backend/Tunnelingtyping.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Tunnelingtyping.v b/backend/Tunnelingtyping.v
index 834e8e1..743b468 100644
--- a/backend/Tunnelingtyping.v
+++ b/backend/Tunnelingtyping.v
@@ -17,7 +17,7 @@ Require Import Maps.
Require Import UnionFind.
Require Import AST.
Require Import Values.
-Require Import Mem.
+Require Import Memory.
Require Import Globalenvs.
Require Import Op.
Require Import Locations.