Documenting the removal of coercions between sig, sigT, sig2,

etc. (source of incompatibility).

1 files changed, 2 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 2088fa6ff7..58cec04ca2 100644
--- a/CHANGES
+++ b/CHANGES
@@ -405,6 +405,8 @@ Libraries
 - SetoidPermutation: a notion of permutation for lists modulo a setoid equality.
 - BigN: fixed the ocaml code doing the parsing/printing of big numbers.
 - List: a couple of lemmas added especially about no-duplication, partitions.
+- Init: Removal of the coercions between variants of sigma-types and
+  subset types (possible source of incompatibility).
 
 Changes from V8.4beta to V8.4beta2
 ==================================