diff options
| author | Jason Gross | 2018-12-05 13:21:52 -0500 |
|---|---|---|
| committer | Jason Gross | 2019-01-24 14:29:03 -0500 |
| commit | 594e53cda3845794bf1e14aec7b0d2a5ee9cd075 (patch) | |
| tree | 6d9e53c251d2a8423ba7e76f0793fd4dbfa31a9c | |
| parent | 4d3ecf1acd584200fe4299b8d12104c7acc33579 (diff) | |
Update CHANGES
| -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 |