diff options
| author | Jason Gross | 2018-08-23 11:03:29 -0400 |
|---|---|---|
| committer | Jason Gross | 2018-08-31 20:05:54 -0400 |
| commit | 6dcbbeb95682bbf470e58e25e0a357a84c3283b6 (patch) | |
| tree | 41abb312099ed7481e16462107f3790b4295f8fb /CHANGES | |
| parent | 548976ac825298f27e6be00bbbb1be0752568f6f (diff) | |
Make Numeral Notation follow Import, not Require
Because that's the sane thing to do.
This will inevitably cause issues for projects which do not `Import
Coq.Strings.Ascii` before trying to use ascii notations.
We also move the syntax plugin for `int31` notations from `Cyclic31` to
`Int31`, so that users (like CompCert) who merely `Require Import
Coq.Numbers.Cyclic.Int31.Int31` get the `int31` numeral syntax. Since
`Cyclic31` `Export`s `Int31`, this should not cause any additional
incompatibilities.
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 18 |
1 files changed, 18 insertions, 0 deletions
@@ -69,6 +69,24 @@ Standard Library `dec_int_scope` and `dec_uint_scope`, to clash less with ssreflect and other packages. They are still delimited by `%int` and `%uint`. +- Syntax notations for `string`, `ascii`, `Z`, `positive`, `N`, `R`, + and `int31` are no longer available merely by `Require`ing the files + that define the inductives. You must `Import` `Coq.Strings.String`, + `Coq.Strings.Ascii`, `Coq.ZArith.BinIntDef`, `Coq.PArith.BinPosDef`, + `Coq.NArith.BinNatDef`, `Coq.Reals.Rdefinitions`, and + `Coq.Numbers.Cyclic.Int31.Int31`, respectively, to be able to use + these notations. Note that passing `-compat 8.8` or issuing + `Require Import Coq.Compat.Coq88` will make these notations + available. Users wishing to port their developments automatically + may download `fix.py` from + <https://gist.github.com/JasonGross/5d4558edf8f5c2c548a3d96c17820169> + and run a command like `while true; do make -Okj 2>&1 | + /path/to/fix.py; done` and get a cup of coffee. (This command must + be manually interrupted once the build finishes all the way though. + Note also that this method is not fail-proof; you may have to adjust + some scopes if you were relying on string notations not being + available even when `string_scope` was open.) + - Numeral syntax for `nat` is no longer available without loading the entire prelude (`Require Import Coq.Init.Prelude`). This only impacts users running Coq without the init library (`-nois` or |