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 /backend/Registers.v | |
parent | e4723d142aa7b1229cdf5989340342d7c5ce870c (diff) | |
download | compcert-05b0e3c922cf7db7ec9313d20193f9cac8fc9358.tar.gz compcert-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 'backend/Registers.v')
0 files changed, 0 insertions, 0 deletions