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.

---
 ia32/Asmgen.v | 13 +++----------
 1 file changed, 3 insertions(+), 10 deletions(-)

(limited to 'ia32/Asmgen.v')

diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v
index 91122898..fd0d5bc5 100644
--- a/ia32/Asmgen.v
+++ b/ia32/Asmgen.v
@@ -12,16 +12,9 @@
 
 (** Translation from Mach to IA32 Asm. *)
 
-Require Import Coqlib.
-Require Import Errors.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Memdata.
-Require Import Op.
-Require Import Locations.
-Require Import Mach.
-Require Import Asm.
+Require Import Coqlib Errors.
+Require Import Integers Floats AST Memdata.
+Require Import Op Locations Mach Asm.
 
 Open Local Scope string_scope.
 Open Local Scope error_monad_scope.
-- 
cgit