1 files changed, 0 insertions, 3 deletions
diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v
index f88f9c0..136a765 100644
--- a/ia32/SelectOpproof.v
+++ b/ia32/SelectOpproof.v
@@ -13,15 +13,12 @@
 (** Correctness of instruction selection for operators *)
 
 Require Import Coqlib.
-Require Import Maps.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
 Require Import Memory.
-Require Import Events.
 Require Import Globalenvs.
-Require Import Smallstep.
 Require Import Cminor.
 Require Import Op.
 Require Import CminorSel.