From 8a02738a47d7dcbf93967b5f8a46f1a0f50f3840 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 19 Apr 2020 13:55:23 +0200
Subject: Slight modification of the partial-order algorithm so that it does
 not remove itself in the set of elements bigger than it if it is indeed the
 case.

This does not impact the warning issued when the recursivity is not
mutual but this produces a result consistent with the unary case when
the order is reflexive (i.e. results of the form (x,Inr[x,y]) happens
also in the mutual case to indicate a cycle x<=y<=x while before we
had results of the form (x,Inr[x]) only in the unary case). I.e.:

Before:
(x,[y]),(y,[x]) -> (x,Inr[]),(y,Inl x)
(x,[x]) -> (x,Inr[x])

Now:
(x,[y]),(y,[x]) -> (x,Inr[x]),(y,Inl x)
(x,[x]) -> (x,Inr[x])
---
 vernac/comFixpoint.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/comFixpoint.ml')

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index e4fa212a23..4c7a706fdb 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -53,7 +53,7 @@ let rec partial_order cmp = function
                     (z, Inr (List.add_set cmp x (List.remove cmp y zge)))
                   else
                     (z, Inr zge)) res in
-            browse ((y,Inl x)::res) xge' (List.union cmp xge (List.remove cmp x yge))
+            browse ((y,Inl x)::res) xge' (List.union cmp xge yge)
           else
             browse res (List.add_set cmp y (List.union cmp xge' yge)) xge
         with Not_found -> browse res (List.add_set cmp y xge') xge
-- 
cgit v1.2.3