diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-12-29 14:44:33 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-12-29 14:46:49 +0100 |
commit | 2e202e2b17cc3ae909628b7b3ae0b8ede3117d82 (patch) | |
tree | 5e567139c9e681bf8f72413c71022eb71b41dedd /aarch64/SelectOpproof.v | |
parent | d4513f41c54869c9b4ba96ab79d50933a1d5c25a (diff) | |
download | compcert-2e202e2b17cc3ae909628b7b3ae0b8ede3117d82.tar.gz compcert-2e202e2b17cc3ae909628b7b3ae0b8ede3117d82.zip |
Remove useless parameters in theorems int_round_odd_bits and int_round_odd_le
IEEE754_extra: clear unused context so that none of the context is
picked up by tactics and ends as extra parameters to theorems
int_round_odd_bits and int_round_odd_le
Floats: simplify uses of int_round_odd_bits and int_round_odd_le
accordingly.
Diffstat (limited to 'aarch64/SelectOpproof.v')
0 files changed, 0 insertions, 0 deletions