summaryrefslogtreecommitdiff
path: root/backend/CleanupLabelsproof.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/CleanupLabelsproof.v')
-rw-r--r--backend/CleanupLabelsproof.v2
1 files changed, 0 insertions, 2 deletions
diff --git a/backend/CleanupLabelsproof.v b/backend/CleanupLabelsproof.v
index a7a60f6..dbd33c1 100644
--- a/backend/CleanupLabelsproof.v
+++ b/backend/CleanupLabelsproof.v
@@ -13,7 +13,6 @@
(** Correctness proof for clean-up of labels *)
Require Import Coqlib.
-Require Import Maps.
Require Import Ordered.
Require Import FSets.
Require Import AST.
@@ -22,7 +21,6 @@ Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Globalenvs.
-Require Import Errors.
Require Import Smallstep.
Require Import Op.
Require Import Locations.