aboutsummaryrefslogtreecommitdiff
path: root/theories/Floats
ModeNameSize
-rw-r--r--FloatAxioms.v3509logplain
-rw-r--r--FloatClass.v780logplain
-rw-r--r--FloatLemmas.v11081logplain
-rw-r--r--FloatOps.v2240logplain
-rw-r--r--Floats.v1439logplain
-rw-r--r--PrimFloat.v5274logplain
-rw-r--r--SpecFloat.v13422logplain