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 /powerpc | |
| parent | d4513f41c54869c9b4ba96ab79d50933a1d5c25a (diff) | |
| download | compcert-kvx-2e202e2b17cc3ae909628b7b3ae0b8ede3117d82.tar.gz compcert-kvx-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 'powerpc')
0 files changed, 0 insertions, 0 deletions