aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/SimplLocals.v
diff options
context:
space:
mode:
Diffstat (limited to 'cfrontend/SimplLocals.v')
-rw-r--r--cfrontend/SimplLocals.v10
1 files changed, 3 insertions, 7 deletions
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.