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/Stacking.v | 16 ++++------------
 1 file changed, 4 insertions(+), 12 deletions(-)

(limited to 'backend/Stacking.v')

diff --git a/backend/Stacking.v b/backend/Stacking.v
index ab67e213..cf797a11 100644
--- a/backend/Stacking.v
+++ b/backend/Stacking.v
@@ -12,18 +12,10 @@
 
 (** Layout of activation records; translation from Linear to Mach. *)
 
-Require Import Coqlib.
-Require Import Errors.
-Require Import AST.
-Require Import Integers.
-Require Import Op.
-Require Import Locations.
-Require Import Linear.
-Require Import Bounds.
-Require Import Mach.
-Require Import Conventions.
-Require Import Stacklayout.
-Require Import Lineartyping.
+Require Import Coqlib Errors.
+Require Import Integers AST.
+Require Import Op Locations Linear Mach.
+Require Import Bounds Conventions Stacklayout Lineartyping.
 
 (** * Layout of activation records *)
 
-- 
cgit