diff options
| author | Jason Gross | 2020-06-20 23:35:53 -0400 |
|---|---|---|
| committer | Jason Gross | 2020-08-09 18:16:37 -0400 |
| commit | fcc3db46303d97e0696a1685619301be3622f4e9 (patch) | |
| tree | 16c19c771b74d7229b0cfcf66557803f54348245 /kernel | |
| parent | ef08abec26c2f0017d1136870f8f99144e579538 (diff) | |
Bring Float notations in line with stdlib
This is a companion to #12479 as per
https://github.com/coq/coq/pull/12479#issuecomment-641336039 that
changes some of the PrimFloat notations:
- `m == n` into `m =? n` to correspond with the eqb notations elsewhere
- `m < n` into `m <? n` to correspond with the ltb notations elsewhere
- `m <= n` into `m <=? n` to correspond with the leb notations elsewhere
We also put them in a module, so users can `Require PrimFloat. Import
PrimFloat.PrimFloatNotations` without needing to unqualify the
primitives.
Fixes the part of #12454 about floats
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions