aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorherbelin2010-06-14 11:53:45 +0000
committerherbelin2010-06-14 11:53:45 +0000
commitb570e389ed7e8765bc61642a94633ce64140c5ed (patch)
treef6a96691fa1e5445a836968d668352fcbb329492
parente07a8f130f599ec6dc85850cf7c7c8709f0fda9a (diff)
Alert on the possible incompatibilties with set_add (see bug 2111) which
was actually used in the contribs (MiniC). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13134 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--CHANGES1
1 files changed, 1 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 128b3dafb3..072a298d2d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -191,6 +191,7 @@ Library
- Definition of Permutation is now in Sorting/Permtation.v
- Some other light revisions and extensions (possible source
of incompatibilities solvable by qualifying names accordingly).
+- In ListSet, set_map has been fixed (source of incompatibilities if used).
- Sorting library:
- new mergesort of worst-case complexity O(n*ln(n)) made available in
Mergesort.v;