summaryrefslogtreecommitdiff
path: root/ia32
diff options
context:
space:
mode:
Diffstat (limited to 'ia32')
-rw-r--r--ia32/Asmgenproof1.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v
index 75d59a4..e3e62cc 100644
--- a/ia32/Asmgenproof1.v
+++ b/ia32/Asmgenproof1.v
@@ -23,7 +23,6 @@ Require Import Globalenvs.
Require Import Op.
Require Import Locations.
Require Import Mach.
-Require Import Machtyping.
Require Import Asm.
Require Import Asmgen.
Require Import Asmgenproof0.