aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/PostpassScheduling.v
diff options
context:
space:
mode:
Diffstat (limited to 'mppa_k1c/PostpassScheduling.v')
-rw-r--r--mppa_k1c/PostpassScheduling.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v
index 8b6de1e2..31180cea 100644
--- a/mppa_k1c/PostpassScheduling.v
+++ b/mppa_k1c/PostpassScheduling.v
@@ -12,7 +12,7 @@
Require Import Coqlib Errors AST Integers.
Require Import Asmblock Axioms Memory Globalenvs.
-Require Import Asmblockdeps Asmblockgenproof0.
+Require Import Asmblockdeps Asmblockgenproof0 Asmblockprops.
Require Peephole.
Local Open Scope error_monad_scope.