diff options
| -rw-r--r-- | CHANGES.md | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/CHANGES.md b/CHANGES.md index 6d76c857c9..cacf0e09e4 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -75,6 +75,11 @@ Tactics foo : database`). When the database name is omitted, the hint is added to the core database (as previously), but a deprecation warning is emitted. +- There is now a tactic in `PreOmega.v` called `Z.div_mod_to_quot_rem` + which allows `lia`, `nia`, `romega`, etc to support `Z.div` and + `Z.modulo`, by posing the specifying equation for `Z.div` and + `Z.modulo` before replacing them with atoms. + Vernacular commands - `Combined Scheme` can now work when inductive schemes are generated in sort @@ -288,11 +293,6 @@ Standard Library impacts users running Coq without the init library (`-nois` or `-noinit`) and also issuing `Require Import Coq.Init.Datatypes`. -- Tactic `zify` (and therefore `lia`, `nia`, `romega`, etc) now - supports `Z.div` and `Z.modulo` via the `Z.div_mod_to_quot_rem` - tactic in `PreOmega.v`, which poses the specifying equation for - `Z.div` and `Z.modulo` before replacing them with atoms. - Tools - Coq_makefile lets one override or extend the following variables from |