aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Alloctyping.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/Alloctyping.v')
-rw-r--r--backend/Alloctyping.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/backend/Alloctyping.v b/backend/Alloctyping.v
index a6536831..59bf621b 100644
--- a/backend/Alloctyping.v
+++ b/backend/Alloctyping.v
@@ -19,6 +19,7 @@ Require Import AST.
Require Import Op.
Require Import Registers.
Require Import RTL.
+Require Import Liveness.
Require Import Locations.
Require Import LTL.
Require Import Coloring.