diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-03-06 10:32:08 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-03-06 10:32:08 +0100 |
| commit | 05b0e3c922cf7db7ec9313d20193f9cac8fc9358 (patch) | |
| tree | 4484af6fc8da464b86d2de49ff1b653a0666ab19 /cfrontend/SimplExpr.v | |
| parent | e4723d142aa7b1229cdf5989340342d7c5ce870c (diff) | |
| download | compcert-kvx-05b0e3c922cf7db7ec9313d20193f9cac8fc9358.tar.gz compcert-kvx-05b0e3c922cf7db7ec9313d20193f9cac8fc9358.zip | |
Define linking for Csyntax and Clight programs.
Also: factor out the type "program" between Csyntax and Clight, putting it in Ctypes.
Diffstat (limited to 'cfrontend/SimplExpr.v')
0 files changed, 0 insertions, 0 deletions