aboutsummaryrefslogtreecommitdiffstats
path: root/lib/IEEE754_extra.v
Commit message (Expand)AuthorAgeFilesLines
* Upgrade to Flocq 4.1.Guillaume Melquiond2022-04-261-2/+2
* Upgrade to Flocq 4.0.Guillaume Melquiond2022-04-251-113/+93
* Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-081-4/+5
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-130/+130
* Remove useless parameters in theorems int_round_odd_bits and int_round_odd_leXavier Leroy2020-12-291-5/+5
* Support the use of already-installed MenhirLib and Flocq librariesXavier Leroy2020-09-211-2/+2
* Rename Fappli_IEEE_extra.v into IEEE754_extra.vXavier Leroy2019-04-261-0/+1515