summaryrefslogtreecommitdiff
path: root/cfrontend/Cminorgen.v
diff options
context:
space:
mode:
Diffstat (limited to 'cfrontend/Cminorgen.v')
-rw-r--r--cfrontend/Cminorgen.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v
index e024caf..af85971 100644
--- a/cfrontend/Cminorgen.v
+++ b/cfrontend/Cminorgen.v
@@ -23,7 +23,6 @@ Require Import Ordered.
Require Import AST.
Require Import Integers.
Require Import Floats.
-Require Import Memdata.
Require Import Csharpminor.
Require Import Cminor.