diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2018-12-03 15:07:05 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-12-20 15:19:42 +0100 |
| commit | 88e9a78529282605f097bff78c6604524d25b592 (patch) | |
| tree | 69369317c7ac2bb0ab32dd6d3a6ca9ba87a60ceb /x86/Asmgenproof1.v | |
| parent | b7fe793fd2427e233ac3da64d0d50334f75a81e6 (diff) | |
| download | compcert-88e9a78529282605f097bff78c6604524d25b592.tar.gz compcert-88e9a78529282605f097bff78c6604524d25b592.zip | |
Add functions "ordered" and "compare" to Float and Float32
"compare" returns the 4 possible results w/ type "option comparison".
"ordered" returns a Boolean.
These functions will be used soon in the x86 port.
Diffstat (limited to 'x86/Asmgenproof1.v')
0 files changed, 0 insertions, 0 deletions