diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-11-14 16:04:03 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-11-14 16:04:03 +0100 |
| commit | 4c471a5a7852d02c368101205b34418c0f754b91 (patch) | |
| tree | eaa336fa65571e440f183c745d7bc40b591050fe /backend/Duplicate.v | |
| parent | 8d1b23070baa3c2db69a066dfc097e08bb811eb3 (diff) | |
| download | compcert-kvx-4c471a5a7852d02c368101205b34418c0f754b91.tar.gz compcert-kvx-4c471a5a7852d02c368101205b34418c0f754b91.zip | |
fixing a potential inconsistency from unsafe_coerce
Now, unsafe_coerce axioms are clearly consistent (for any interpretation of may-return monads).
But, the extraction is still unsafe...
Diffstat (limited to 'backend/Duplicate.v')
0 files changed, 0 insertions, 0 deletions