diff options
Diffstat (limited to 'dev/doc/changes.md')
| -rw-r--r-- | dev/doc/changes.md | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 8a2a2fffc6..5be8257e87 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -1,5 +1,17 @@ ## Changes between Coq 8.7 and Coq 8.8 +### Bug tracker + +As of 18/10/2017, Coq uses [GitHub issues](https://github.com/coq/coq/issues) +as bug tracker. +Old bug reports were migrated from Bugzilla to GitHub issues using +[this migration script](https://gist.github.com/Zimmi48/d923e52f64fe17c72852d9c148bfcdc6#file-bugzilla2github) +as detailed in [this blog post](https://www.theozimmermann.net/2017/10/bugzilla-to-github/). + +All the bugs with a number below 1154 had to be renumbered, you can find +a correspondence table [here](/dev/bugzilla2github_stripped.csv). +All the other bugs kept their number. + ### Plugin API Coq 8.8 offers a new module overlay containing a proposed plugin API @@ -32,6 +44,19 @@ We renamed the following datatypes: - `Pp.std_ppcmds` -> `Pp.t` +Some tactics and related functions now support static configurability, e.g.: + +- injectable, dEq, etc. takes an argument ~keep_proofs which, + - if None, tells to behave as told with the flag Keep Proof Equalities + - if Some b, tells to keep proof equalities iff b is true + +Declaration of printers for arguments used only in vernac command + +- It should now use "declare_extra_vernac_genarg_pprule" rather than + "declare_extra_genarg_pprule", otherwise, a failure at runtime might + happen. An alternative is to register the corresponding argument as + a value, using "Geninterp.register_val0 wit None". + ## Changes between Coq 8.6 and Coq 8.7 ### Ocaml |