diff options
Diffstat (limited to 'ChangeLog')
| -rw-r--r-- | ChangeLog | 11 |
1 files changed, 6 insertions, 5 deletions
@@ -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 |