From 21613d7ad098ce4a080963aa4210ce208d24e9b3 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Sun, 6 Mar 2016 10:33:19 +0100
Subject: Update the proofs of the C front-end to the new linking framework.

---
 cfrontend/SimplLocals.v | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

(limited to 'cfrontend/SimplLocals.v')

diff --git a/cfrontend/SimplLocals.v b/cfrontend/SimplLocals.v
index c4b1054d..580f02c2 100644
--- a/cfrontend/SimplLocals.v
+++ b/cfrontend/SimplLocals.v
@@ -15,13 +15,9 @@
 
 Require Import FSets.
 Require FSetAVL.
-Require Import Coqlib.
-Require Import Ordered.
-Require Import Errors.
-Require Import AST.
-Require Import Ctypes.
-Require Import Cop.
-Require Import Clight.
+Require Import Coqlib Ordered Errors.
+Require Import AST Linking.
+Require Import Ctypes Cop Clight.
 Require Compopts.
 
 Open Scope error_monad_scope.
-- 
cgit