diff options
| author | Hugo Herbelin | 2020-04-19 13:55:23 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-01 23:17:27 +0200 |
| commit | 8a02738a47d7dcbf93967b5f8a46f1a0f50f3840 (patch) | |
| tree | 90b52ab4f10ec4b863087fd44cccbe59135f4989 /vernac/comFixpoint.ml | |
| parent | f129326d545ae27d362132b279167d119894a992 (diff) | |
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])
Diffstat (limited to 'vernac/comFixpoint.ml')
| -rw-r--r-- | vernac/comFixpoint.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |