diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-05-31 19:07:47 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-06-06 10:58:13 +0200 |
| commit | b028cfb4a2c342a49e165fa2267176feec7977ed (patch) | |
| tree | 43b35a0ca7aeb4d0eb684d7b1dac84980c2b5708 /backend/Cminortyping.v | |
| parent | 26775b65ba98ad798fc72c92ae73bd28609aaeb8 (diff) | |
| download | compcert-kvx-b028cfb4a2c342a49e165fa2267176feec7977ed.tar.gz compcert-kvx-b028cfb4a2c342a49e165fa2267176feec7977ed.zip | |
Additional simulation diagrams for determinate source languages
If the source language is determinate, it can take several steps
(not just one) before the "match_state" invariant is reinstated.
Diffstat (limited to 'backend/Cminortyping.v')
0 files changed, 0 insertions, 0 deletions