aboutsummaryrefslogtreecommitdiff
path: root/theories/Floats/FloatOps.v
AgeCommit message (Expand)Author
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-26Consolidate int63-related notationsMaxime Dénès
2019-11-01Fix ldshiftexpPierre Roux
2019-11-01docs: Add refman+stdlib documentationErik Martin-Dorel
2019-11-01Add next_{up,down} primitive float functionsPierre Roux
2019-11-01Put axioms on ldshiftexp and frshiftexpGuillaume Bertholon