From d69ec6e2e0931a87d2ec3b3f47d1969b365d91f7 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 5 Dec 2018 16:05:13 -0500
Subject: Rename Z.div_mod_to_quot_rem, add Z.quot_rem_to_equations,
 Z.to_euclidean_division_equations

---
 CHANGES.md | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

(limited to 'CHANGES.md')

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
 
-- 
cgit v1.2.3