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 /doc/changelog | |
| 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 'doc/changelog')
| -rw-r--r-- | doc/changelog/10-standard-library/12556-fix-float-ltb-notations.rst | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/doc/changelog/10-standard-library/12556-fix-float-ltb-notations.rst b/doc/changelog/10-standard-library/12556-fix-float-ltb-notations.rst new file mode 100644 index 0000000000..1709cf1eae --- /dev/null +++ b/doc/changelog/10-standard-library/12556-fix-float-ltb-notations.rst @@ -0,0 +1,9 @@ +- **Changed:** + PrimFloat notations now match up with the rest of the standard library: :g:`m + == n`, :g:`m < n`, and :g:`m <= n` have been replaced with :g:`m =? n`, :g:`m + <? n`, and :g:`m <=? n`. The old notations are still available as deprecated + notations. Additionally, there is now a + ``Coq.Floats.PrimFloat.PrimFloatNotations`` module that users can import to + get the ``PrimFloat`` notations without unqualifying the various primitives + (`#12556 <https://github.com/coq/coq/pull/12556>`_, fixes `#12454 + <https://github.com/coq/coq/issues/12454>`_, by Jason Gross). |