From e4723d142aa7b1229cdf5989340342d7c5ce870c Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Sun, 6 Mar 2016 10:31:26 +0100
Subject: Update the back-end proofs to the new linking framework.

---
 backend/Linearize.v | 16 +++-------------
 1 file changed, 3 insertions(+), 13 deletions(-)

(limited to 'backend/Linearize.v')

diff --git a/backend/Linearize.v b/backend/Linearize.v
index 68c2b32f..2cfa4d3c 100644
--- a/backend/Linearize.v
+++ b/backend/Linearize.v
@@ -12,19 +12,9 @@
 
 (** Linearization of the control-flow graph: translation from LTL to Linear *)
 
-Require Import Coqlib.
-Require Import Maps.
-Require Import Ordered.
-Require Import FSets.
-Require FSetAVL.
-Require Import AST.
-Require Import Errors.
-Require Import Op.
-Require Import Locations.
-Require Import LTL.
-Require Import Linear.
-Require Import Kildall.
-Require Import Lattice.
+Require Import FSets FSetAVL.
+Require Import Coqlib Maps Ordered Errors Lattice Kildall.
+Require Import AST Op Locations LTL Linear.
 
 Open Scope error_monad_scope.
 
-- 
cgit