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/SimplExpr.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/SimplExpr.v')
-rw-r--r-- | cfrontend/SimplExpr.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index a5a6ad66..c88c4db5 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -512,9 +512,9 @@ Local Open Scope error_monad_scope. Definition transl_fundef (fd: Csyntax.fundef) : res fundef := match fd with - | Csyntax.Internal f => + | Internal f => do tf <- transl_function f; OK (Internal tf) - | Csyntax.External ef targs tres cc => + | External ef targs tres cc => OK (External ef targs tres cc) end. @@ -523,6 +523,6 @@ Definition transl_program (p: Csyntax.program) : res program := OK {| prog_defs := AST.prog_defs p1; prog_public := AST.prog_public p1; prog_main := AST.prog_main p1; - prog_types := Csyntax.prog_types p; - prog_comp_env := Csyntax.prog_comp_env p; - prog_comp_env_eq := Csyntax.prog_comp_env_eq p |}. + prog_types := prog_types p; + prog_comp_env := prog_comp_env p; + prog_comp_env_eq := prog_comp_env_eq p |}. |