Document change on comparison predicates in order.v

1 files changed, 31 insertions, 0 deletions

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 6d2d74f..58cd473 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -92,6 +92,37 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
     1.10 in newer versions by using the `mc_1_10.Num` module instead of the
     `Num` module. However, instances of the number structures may require
     changes.
+  + In the development process of this version of Mathematical Components, the
+    ordering of arguments of comparison predicates `lcomparableP`,
+    `(lcomparable_)ltgtP`, `(lcomparable_)leP`, and `(lcomparable_)ltP` in
+    `order.v` has been changed as follows. This is a potential source of
+    incompatibilities.
+    * before the change:
+      ```
+      lcomparableP x y : incomparel x y
+        (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y)
+        (y >=< x) (x >=< y) (y `&` x) (x `&` y) (y `|` x) (x `|` y).
+      ltgtP x y : comparel x y
+        (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y)
+        (y `&` x) (x `&` y) (y `|` x) (x `|` y).
+      leP x y :
+        lel_xor_gt x y (x <= y) (y < x) (y `&` x) (x `&` y) (y `|` x) (x `|` y).
+      ltP x y :
+        ltl_xor_ge x y (y <= x) (x < y) (y `&` x) (x `&` y) (y `|` x) (x `|` y).
+      ```
+    * after the change:
+      ```
+      lcomparableP x y : incomparel x y
+        (y `&` x) (x `&` y) (y `|` x) (x `|` y)
+        (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y) (y >=< x) (x >=< y).
+      ltgtP x y : comparel x y
+        (y `&` x) (x `&` y) (y `|` x) (x `|` y)
+        (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y).
+      leP x y :
+        lel_xor_gt x y (y `&` x) (x `&` y) (y `|` x) (x `|` y) (x <= y) (y < x).
+      ltP x y :
+        ltl_xor_ge x y (y `&` x) (x `&` y) (y `|` x) (x `|` y) (y <= x) (x < y).
+      ```
 
 - Extended comparison predicates `leqP`, `ltnP`, and `ltngtP` in ssrnat to
   allow case analysis on `minn` and `maxn`.