aboutsummaryrefslogtreecommitdiff
path: root/theories/Floats/FloatOps.v
AgeCommit message (Expand)Author
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