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. * 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 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 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) * Renamed/generalized: mul_Sm_binm -> mul_bin_diag divn1 -> divz1 (in intdiv) rootC -> nthroot 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, 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 that is relevant to her. Note that this introduces a possible incompatibility for users of the previous version. A replacement scheme is suggested in the installation notes. * The archive is now open and based on git. Public mirror at: https://github.com/math-comp/math-comp * Sources of the reference manual of the Ssreflect tactic language are also open and available at: https://github.com/math-comp/ssr-manual Pull requests improving the documentation are welcome. * Renaming or replacements: conjC_closed -> cfConjC_closed class_transr -> class_eqP cfclass_transl -> cfclass_transr nontrivial_ideal -> proper_ideal zchar_orthonormalP -> vchar_orthonormalP * Definitions that changed: seq_sub * Statements that changed: orbit_in_transl, orbit_sym, orbit_trans, orbit_transl, orbit_transr, cfAut_char, cfConjC_char, invg_lcosets, lcoset_transl, lcoset_transr, rcoset_transl, rcoset_transr, mem2_last, bind_unless, unless_contra, all_and2, all_and3, all_and4, all_and5, ltr0_neq0, ltr_prod, Zisometry_of_iso * New definitions: adhoc_seq_sub_choiceMixin, adhoc_seq_sub_[choice|fin]Type * New theorems: orbit_in_eqP, cards_draws, cfAut_lin_char, cfConjC_lin_char, extend_cfConjC_subset, isometry_of_free, cfAutK, cfAutVK, lcoset_eqP, rcoset_eqP, class_eqP, gFsub_trans, gFnorms, gFchar_trans, gFnormal_trans, gFnorm_trans, mem2_seq1, dvdn_fact, prime_above, subKr, subrI, subIr, subr0_eq, divrI, divIr, divKr, divfI, divIf, divKf, impliesP, impliesPn, unlessL, unlessR, unless_sym, unlessP (coercion), classicW, ltr_prod_nat * New notation: "\unless C, P" 12/03/2014 - split the archive in SSReflect and MathComp - version 1.5 * With this release "ssreflect" has been split into two packages. The Ssreflect one contains the proof language (plugin for Coq) and a small set of core theory libraries about boolean, natural numbers, sequences, decidable equality and finite types. The Mathematical Components one contains advanced theory files covering a wider spectrum of mathematics. * With respect to version 1.4 the proof language got a few new 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. 05/09/2012 - ssreflect - version 1.4 * With this release the plugin code received many bug fixes and the existing libraries relevant updates. This release also includes some new libraries on the following topics: rational numbers, divisibility of integers, F-algebras, finite dimensional field extensions and Euclidean division for polynomials over a ring. * The release includes a major code refactoring of the plugin for Coq 8.4. In particular a documented ML API to access the pattern matching facilities of Ssreflect from third party plugins has been introduced. 14/03/2011 - ssreflect - version 1.3 * The tactic language has been extended with several new features, inspired by the five years of intensive use in our project. However we have kept the core of the language unchanged; the new library compiles with Ssreflect 1.2. Users of a Coq 8.2 toplevel statically linked with Ssreflect 1.2 need to comment the Declare ML Module "ssreflect" line in ssreflect.v to properly compile the 1.3 library. We will continue supporting new releases of Coq in due course. * The new library adds general linear algebra (matrix rank, subspaces) and all of the advanced finite group that was developed in the course of completing the Local Analysis part of the Odd Order Theorem, starting from the Sylow and Hall theorems and including full structure theorems for abelian, extremal and extraspecial groups, and general (modular) linear representation theory. 14/08/2009 - ssreflect - version 1.2 * No change log 18/03/2008 - ssreflect - version 1.1 * First public release