diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2014-11-26 14:46:07 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2014-11-26 14:46:07 +0100 |
| commit | b279716c76c387c6c5eec96388c0c35629858b4c (patch) | |
| tree | a71079afbe6eebc1162391546aeaebe56dbd56d2 /cfrontend/SimplExprproof.v | |
| parent | 1ccc058794381d7d7c2ff704786009019489001d (diff) | |
| download | compcert-kvx-b279716c76c387c6c5eec96388c0c35629858b4c.tar.gz compcert-kvx-b279716c76c387c6c5eec96388c0c35629858b4c.zip | |
Introduce symbol environments (type Senv.t) as a restricted view on global environments (type Genv.t). Use symbol environments instead of global environments for external functions (module Events).
Diffstat (limited to 'cfrontend/SimplExprproof.v')
| -rw-r--r-- | cfrontend/SimplExprproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 250f2b26..6d8b5c86 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -91,9 +91,9 @@ Proof. Qed. Lemma block_is_volatile_preserved: - forall b, block_is_volatile tge b = block_is_volatile ge b. + forall b, Genv.block_is_volatile tge b = Genv.block_is_volatile ge b. Proof. - intros. unfold block_is_volatile. rewrite varinfo_preserved. auto. + intros. unfold Genv.block_is_volatile. rewrite varinfo_preserved. auto. Qed. Lemma type_of_fundef_preserved: |