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/Cminorgen.v | |
| parent | 05b0e3c922cf7db7ec9313d20193f9cac8fc9358 (diff) | |
| download | compcert-kvx-21613d7ad098ce4a080963aa4210ce208d24e9b3.tar.gz compcert-kvx-21613d7ad098ce4a080963aa4210ce208d24e9b3.zip | |
Update the proofs of the C front-end to the new linking framework.
Diffstat (limited to 'cfrontend/Cminorgen.v')
| -rw-r--r-- | cfrontend/Cminorgen.v | 17 |
1 files changed, 4 insertions, 13 deletions
diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index c2b59fbe..b9a28ee1 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -12,19 +12,10 @@ (** Translation from Csharpminor to Cminor. *) -Require Import FSets. -Require FSetAVL. -Require Import Orders. -Require Mergesort. -Require Import Coqlib. -Require Import Errors. -Require Import Maps. -Require Import Ordered. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Csharpminor. -Require Import Cminor. +Require Import FSets FSetAVL Orders Mergesort. +Require Import Coqlib Maps Ordered Errors Integers Floats. +Require Import AST Linking. +Require Import Csharpminor Cminor. Local Open Scope string_scope. Local Open Scope error_monad_scope. |