From 9e634929e54c703f67cb8e0e3a89ca4099f45470 Mon Sep 17 00:00:00 2001
From: Enrico
Date: Tue, 24 Apr 2018 15:10:24 +0200
Subject: Update ChangeLog

---
 ChangeLog | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index b94fe26..050af89 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,7 +1,7 @@
-23/04/2018 - compatibility with Coq 8.7 and several small fixes -
-	upcoming version 1.7
-	* Compatibility with Coq 8.8
-	* Lost compatibility with Coq <= 8.5
+24/04/2018 - compatibility with Coq 8.8 and several small fixes - version 1.7
+
+	* Added compatibility with Coq 8.8 and lost compatibility with
+	  Coq <= 8.5. This release is compatible with Coq 8.6, 8.7 and 8.8.
 
 	* Integration to Coq: ssrbool.v ssrfun.v and plugin.
 	  ssrtest also moved to Coq test suite.
@@ -23,7 +23,7 @@
 	  implicit, parameter of type numClosedFieldType. This could break
 	  some proofs.
 
-	Lemma dvdn_fact was moved from library prime.v to library div.v
+	* Lemma dvdn_fact was moved from library prime.v to library div.v
 
 	* Structures, changes in interfaces:
 	  numClosedFieldType
@@ -52,6 +52,7 @@
 	  ltngtP, contra_eq, contra_neq, odd_opp, nth_iota
 
 24/11/2015 - major reorganization of the archive - version 1.6
+
 	* Files split into sub-directories: ssreflect, algebra, fingroup,
 	  solvable, field and character. In this way the user can decide
 	  to compile only the subset of the Mathematical Components library
-- 
cgit v1.2.3


From f36bb9b4f35286c5dd2b8e047ba294b47652823b Mon Sep 17 00:00:00 2001
From: Enrico
Date: Tue, 24 Apr 2018 15:15:25 +0200
Subject: fix typo

thanks Yves---
 ChangeLog | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/ChangeLog b/ChangeLog
index 050af89..13045e9 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -17,7 +17,7 @@
 	  conjC, n.-root and sqrtC, previously defined in library algC.v,
 	  are now part of this generic interface. In case of ambiguity,
 	  a cast to type algC, of complex algebraic numbers, can be used to
-	  desambiguate via  typing constraints. Some theory was thus made
+	  disambiguate via  typing constraints. Some theory was thus made
 	  more generic, and the corresponding lemmas, previously defined in
 	  library algC.v (e.g. conjCK) now feature an extra, non maximal
 	  implicit, parameter of type numClosedFieldType. This could break
-- 
cgit v1.2.3