aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Allocation.v
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2016-03-06 10:31:26 +0100
committerXavier Leroy <xavier.leroy@inria.fr>2016-03-06 10:31:26 +0100
commite4723d142aa7b1229cdf5989340342d7c5ce870c (patch)
tree988bdd3027231544239cdac13313c587e9ec83b9 /backend/Allocation.v
parenta803f6926dc6d817447b3926cc409913e5d86cc0 (diff)
downloadcompcert-kvx-e4723d142aa7b1229cdf5989340342d7c5ce870c.tar.gz
compcert-kvx-e4723d142aa7b1229cdf5989340342d7c5ce870c.zip
Update the back-end proofs to the new linking framework.
Diffstat (limited to 'backend/Allocation.v')
-rw-r--r--backend/Allocation.v23
1 files changed, 4 insertions, 19 deletions
diff --git a/backend/Allocation.v b/backend/Allocation.v
index 7534e23f..6a6c1eb6 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -12,26 +12,11 @@
(** Register allocation by external oracle and a posteriori validation. *)
-Require Import FSets.
-Require FSetAVLplus.
+Require Import FSets FSetAVLplus.
+Require Import Coqlib Ordered Maps Errors Integers Floats.
+Require Import AST Lattice Kildall Memdata.
Require Archi.
-Require Import Coqlib.
-Require Import Ordered.
-Require Import Errors.
-Require Import Maps.
-Require Import Lattice.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Memdata.
-Require Import Op.
-Require Import Registers.
-Require Import RTL.
-Require Import Kildall.
-Require Import Locations.
-Require Import Conventions.
-Require Import RTLtyping.
-Require Import LTL.
+Require Import Op Registers RTL Locations Conventions RTLtyping LTL.
(** The validation algorithm used here is described in
"Validating register allocation and spilling",