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 /test-suite/bugs | |
| 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 'test-suite/bugs')
| -rw-r--r-- | test-suite/bugs/closed/bug_12483.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/bug_12483.v b/test-suite/bugs/closed/bug_12483.v index 0d034a65eb..ae46117e59 100644 --- a/test-suite/bugs/closed/bug_12483.v +++ b/test-suite/bugs/closed/bug_12483.v @@ -4,7 +4,7 @@ Goal False. Proof. cut (false = true). { intro H; discriminate H. } -change false with (1 <= 0)%float. +change false with (1 <=? 0)%float. rewrite leb_spec. Fail reflexivity. Abort. |