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/Debugvar.v | 15 +++------------
 1 file changed, 3 insertions(+), 12 deletions(-)

(limited to 'backend/Debugvar.v')

diff --git a/backend/Debugvar.v b/backend/Debugvar.v
index dcc4327a..5d31831a 100644
--- a/backend/Debugvar.v
+++ b/backend/Debugvar.v
@@ -13,18 +13,9 @@
 (** Computation of live ranges for local variables that carry
     debugging information. *)
 
-Require Import Coqlib.
-Require Import Axioms.
-Require Import Maps.
-Require Import Iteration.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Errors.
-Require Import Machregs.
-Require Import Locations.
-Require Import Conventions.
-Require Import Linear.
+Require Import Axioms Coqlib Maps Iteration Errors.
+Require Import Integers Floats AST.
+Require Import Machregs Locations Conventions Linear.
 
 (** A debug info is a [builtin_arg loc] expression that safely evaluates
    in any context. *)
-- 
cgit