From 5f1229849aa90f64cf0126f47c622152383ba118 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Mon, 16 Mar 2020 17:39:00 +0900
Subject: Document change on comparison predicates in order.v

---
 CHANGELOG_UNRELEASED.md | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)

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