diff options
| author | Jason Gross | 2018-12-05 16:05:13 -0500 |
|---|---|---|
| committer | Jason Gross | 2019-01-24 14:31:52 -0500 |
| commit | d69ec6e2e0931a87d2ec3b3f47d1969b365d91f7 (patch) | |
| tree | 6d9502307081d52dd8e00ab53142b1c7f1b54854 /CHANGES.md | |
| parent | 594e53cda3845794bf1e14aec7b0d2a5ee9cd075 (diff) | |
Rename Z.div_mod_to_quot_rem, add Z.quot_rem_to_equations, Z.to_euclidean_division_equations
Diffstat (limited to 'CHANGES.md')
| -rw-r--r-- | CHANGES.md | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/CHANGES.md b/CHANGES.md index cacf0e09e4..54acb610bb 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -75,10 +75,13 @@ 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. +- There are now tactics in `PreOmega.v` called + `Z.div_mod_to_equations`, `Z.quot_rem_to_equations`, and + `Z.to_euclidean_division_equations` (which combines the `div_mod` + and `quot_rem` variants) which allow `lia`, `nia`, `romega`, etc to + support `Z.div` and `Z.modulo` (`Z.quot` and `Z.rem`, respectively), + by posing the specifying equation for `Z.div` and `Z.modulo` before + replacing them with atoms. Vernacular commands |