diff options
| author | Enrico | 2018-04-24 15:10:24 +0200 |
|---|---|---|
| committer | GitHub | 2018-04-24 15:10:24 +0200 |
| commit | 9e634929e54c703f67cb8e0e3a89ca4099f45470 (patch) | |
| tree | b46e0bb76c9bb9d9706c9abb7f366c9e6b10081f /ChangeLog | |
| parent | 78040f8ea61531f564f56224a5590df254828027 (diff) | |
Update ChangeLog
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 |