From 96c8cc8200ca186c19eb7457c9b3f97433772390 Mon Sep 17 00:00:00 2001 From: Assia Mahboubi Date: Mon, 23 Apr 2018 15:01:00 +0200 Subject: Improved ChangeLog One paragraph per version + spell check --- ChangeLog | 65 ++++++++++++++++++++++++++++++--------------------------------- 1 file changed, 31 insertions(+), 34 deletions(-) diff --git a/ChangeLog b/ChangeLog index 12d6ef4..6e9ef59 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,52 +1,49 @@ 07/09/2016 - compatibility with Coq 8.7 and several small fixes - - version 1.6.2 and upcomming version 1.7 + upcoming version 1.7 * Compatibility with Coq 8.7 * Lost compatibility with Coq 8.4 -07/09/2016 - compatibility with Coq 8.7 and several small fixes - - upcomming version 1.7 + * Library refactoring: algC, complex, ssrnum: Library ssrnum.v now + provides an interface numClosedFieldType, which factors some + theory from both complex and algC. In particular, Re, Im, 'i, + conjC, n.-root and sqrtC are now part of this generic + interface. In case of ambiguity, they can be casted to the type + algC, of complex algebraic numbers, 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 + (C : numClosedFieldType). This could break some + proofs. Additionally, a few ad hoc constructions in library + complex.v, e.g. -*+ or complex.Re, are now deprecated and should + be replaced by the corresponding ones provided by the + numClosedFieldType interface. The next revision might definitely + hide those constructions under a module. + + * Structures, changes in interfaces: + numClosedFieldType + * New Theorems: dec_factor_theorem, abstract_context, mul_bin_down, mul_bin_left - * Renamings or replacements: + * Renamed/generalized: mul_Sm_binm -> mul_bin_diag divn1 -> divz1 (in intdiv) - - * Generalized or extended: - ltngtP, contra_eq, contra_neq, odd_opp - - * Plugin: - ssrpattern: compose nicely with Tactic Notation - -25/08/2016 - refactoring of algC and complex in ssrnum - - upcomming version 1.7 - * ssrnum's interface numClosedFieldType factors some theory from - both complex and algC. Because of that Re, Im, 'i, conjC, n.-root - and sqrtC are not specialized to algC anymore. In case of - ambiguity, they should be instanciated with algC using typing - constraints. Moreoever all the lemmas from ssrnum that used to - be in algC (like conjCK), now take an extra nonmaximal implicit - argument (C : numClosedFieldType) which could break some proofs. - Additionally, ad-hoc constructions from complex.v like -*+ or - complex.Re are now deprecated and one should rely solely on the - ssrnum interface. The next revision might definietly hide those - constructions under a module. - - * Structures that change: - numClosedFieldType - - * Renamed and generalized definitions: rootC -> nthroot algRe -> Re algIm -> Im algCi -> imaginaryC - - * Renamed and generalized theorems: Every theorem from ssrnum that used to be in algC + * Generalized or improved: + ltngtP, contra_eq, contra_neq, odd_opp + + * Plugin: + ssrpattern: compatibility with Tactic Notation + + 24/11/2015 - major reorganization of the archive - version 1.6 - * Files split into subdirectories: ssreflect, algebra, fingroup, + * 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 that is relevant to her. Note that this introduces a possible @@ -61,7 +58,7 @@ https://github.com/math-comp/ssr-manual Pull requests improving the documentation are welcome. - * Renamings or replacements: + * Renaming or replacements: conjC_closed -> cfConjC_closed class_transr -> class_eqP cfclass_transl -> cfclass_transr @@ -102,7 +99,7 @@ spectrum of mathematics. * With respect to version 1.4 the proof language got a few new - features related to forward reasoning and some bugfixes. The + features related to forward reasoning and some bug fixes. The Mathematical Components library features 16 new theory files and in particular: some field and Galois theory, advanced character theory and a construction of algebraic numbers. -- cgit v1.2.3 From ca20c413705035862409c6ec7f80ea390e6cd78c Mon Sep 17 00:00:00 2001 From: Assia Mahboubi Date: Mon, 23 Apr 2018 16:16:09 +0200 Subject: Latest changes added to change log. --- ChangeLog | 34 +++++++++++++++++++++++++--------- 1 file changed, 25 insertions(+), 9 deletions(-) diff --git a/ChangeLog b/ChangeLog index 6e9ef59..c6352b2 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,11 +1,18 @@ -07/09/2016 - compatibility with Coq 8.7 and several small fixes - +23/04/2018 - compatibility with Coq 8.7 and several small fixes - upcoming version 1.7 - * Compatibility with Coq 8.7 + * Compatibility with Coq 8.8 (and >= 8.6) * Lost compatibility with Coq 8.4 - * Library refactoring: algC, complex, ssrnum: Library ssrnum.v now + * Integration to Coq: ssrbool.v ssrfun.v and plugin. + ssrtest also moved to Coq test suite. + + * Library refactoring: + odd_order and real_closed: are now in separate repositories. + + algC, complex, ssrnum: Library ssrnum.v now provides an interface numClosedFieldType, which factors some - theory from both complex and algC. In particular, Re, Im, 'i, + theory from both library complex.v (now in the real_closed + repository) and algC. In particular, Re, Im, 'i, conjC, n.-root and sqrtC are now part of this generic interface. In case of ambiguity, they can be casted to the type algC, of complex algebraic numbers, via typing constraints. Some @@ -19,12 +26,20 @@ numClosedFieldType interface. The next revision might definitely hide those constructions under a module. + Lemma dvdn_fact moved from prime to div + * Structures, changes in interfaces: numClosedFieldType * New Theorems: - dec_factor_theorem, abstract_context, - mul_bin_down, mul_bin_left + iter_in, finv_in, inv_f_in, finv_inj_in, fconnect_sym_in, + iter_order_in, iter_finv_in, cycle_orbit_in, fpath_finv_in, + fpath_finv_f_in, fpath_f_finv_in + big_allpairs + uniqP, uniqPn + dec_factor_theorem, + mul_bin_down, mul_bin_left + abstract_context (now merged in Coq) * Renamed/generalized: mul_Sm_binm -> mul_bin_diag @@ -33,14 +48,15 @@ algRe -> Re algIm -> Im algCi -> imaginaryC + reshape_index_leq -> reshape_leq Every theorem from ssrnum that used to be in algC * Generalized or improved: - ltngtP, contra_eq, contra_neq, odd_opp + ltngtP, contra_eq, contra_neq, odd_opp, nth_iota * Plugin: - ssrpattern: compatibility with Tactic Notation - + ssrpattern: compatibility with Tactic Notation + rewrite /foo now allows foo to be a primitive projection. 24/11/2015 - major reorganization of the archive - version 1.6 * Files split into sub-directories: ssreflect, algebra, fingroup, -- cgit v1.2.3 From a8f540454ed463edb48952f9c620484e9c3b6cc1 Mon Sep 17 00:00:00 2001 From: Assia Mahboubi Date: Tue, 24 Apr 2018 12:44:29 +0200 Subject: Removed content about files not in the repo/release + minor stuff --- ChangeLog | 63 ++++++++++++++++++++++++++++----------------------------------- 1 file changed, 28 insertions(+), 35 deletions(-) diff --git a/ChangeLog b/ChangeLog index c6352b2..b94fe26 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,45 +1,42 @@ 23/04/2018 - compatibility with Coq 8.7 and several small fixes - upcoming version 1.7 - * Compatibility with Coq 8.8 (and >= 8.6) - * Lost compatibility with Coq 8.4 + * Compatibility with Coq 8.8 + * Lost compatibility with Coq <= 8.5 * Integration to Coq: ssrbool.v ssrfun.v and plugin. ssrtest also moved to Coq test suite. - * Library refactoring: - odd_order and real_closed: are now in separate repositories. - - algC, complex, ssrnum: Library ssrnum.v now - provides an interface numClosedFieldType, which factors some - theory from both library complex.v (now in the real_closed - repository) and algC. In particular, Re, Im, 'i, - conjC, n.-root and sqrtC are now part of this generic - interface. In case of ambiguity, they can be casted to the type - algC, of complex algebraic numbers, 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 - (C : numClosedFieldType). This could break some - proofs. Additionally, a few ad hoc constructions in library - complex.v, e.g. -*+ or complex.Re, are now deprecated and should - be replaced by the corresponding ones provided by the - numClosedFieldType interface. The next revision might definitely - hide those constructions under a module. - - Lemma dvdn_fact moved from prime to div + * Cleaning up the github repository: the math-comp repository is + now dedicated to the released material (as in the present + release). For instance, directories real-closed and odd-order now + have their own repository. + + * Library refactoring: algC ssrnum: Library ssrnum.v now + provides an interface numClosedFieldType, which abstracts the + theory of algebraic numbers. In particular, Re, Im, 'i, + 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 + 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 + some proofs. + + Lemma dvdn_fact was moved from library prime.v to library div.v * Structures, changes in interfaces: numClosedFieldType * New Theorems: - iter_in, finv_in, inv_f_in, finv_inj_in, fconnect_sym_in, - iter_order_in, iter_finv_in, cycle_orbit_in, fpath_finv_in, - fpath_finv_f_in, fpath_f_finv_in - big_allpairs - uniqP, uniqPn - dec_factor_theorem, - mul_bin_down, mul_bin_left - abstract_context (now merged in Coq) + iter_in, finv_in, inv_f_in, finv_inj_in, fconnect_sym_in, + iter_order_in, iter_finv_in, cycle_orbit_in, fpath_finv_in, + fpath_finv_f_in, fpath_f_finv_in + big_allpairs + uniqP, uniqPn + dec_factor_theorem, + mul_bin_down, mul_bin_left + abstract_context (now merged in Coq) * Renamed/generalized: mul_Sm_binm -> mul_bin_diag @@ -54,10 +51,6 @@ * Generalized or improved: ltngtP, contra_eq, contra_neq, odd_opp, nth_iota - * Plugin: - ssrpattern: compatibility with Tactic Notation - rewrite /foo now allows foo to be a primitive projection. - 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 -- cgit v1.2.3