diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-03-06 10:33:19 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-03-06 10:33:19 +0100 |
| commit | 21613d7ad098ce4a080963aa4210ce208d24e9b3 (patch) | |
| tree | 78b8268691aac4afaa4aa473de260cd562fbb615 /cfrontend/SimplLocals.v | |
| parent | 05b0e3c922cf7db7ec9313d20193f9cac8fc9358 (diff) | |
| download | compcert-21613d7ad098ce4a080963aa4210ce208d24e9b3.tar.gz compcert-21613d7ad098ce4a080963aa4210ce208d24e9b3.zip | |
Update the proofs of the C front-end to the new linking framework.
Diffstat (limited to 'cfrontend/SimplLocals.v')
| -rw-r--r-- | cfrontend/SimplLocals.v | 10 |
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. |