summaryrefslogtreecommitdiff
path: root/cfrontend/Cminorgenproof.v
diff options
context:
space:
mode:
Diffstat (limited to 'cfrontend/Cminorgenproof.v')
-rw-r--r--cfrontend/Cminorgenproof.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 018fcec..62690d6 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -23,7 +23,6 @@ Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
-Require Import Memdata.
Require Import Memory.
Require Import Events.
Require Import Globalenvs.