aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-11-29update changelogs for the 1.10.0 releaseYves Bertot
2019-11-29Return of PR #226: adds relevant theorems when fcycle f (orbit f x) and the ↵Cyril Cohen
needed lemmas (#261) * adds relevant theorems when fcycle f (orbit f x) and the needed lemmas * Generalize f_step lemmas * Generalizations, shorter proofs, bugfixes, CHANGELOG - changelog, renamings and comments - renaming `homo_cycle` to `mem_fcycle` and other small renamings - name swap `mem_orbit` and `in_orbit` - simplifications - generalization following @pi8027's comment - Getting rid of many uniquness condition in `fingraph.v` - added cases to the equivalence `orbitPcycle` - added `cycle_catC`
2019-11-29Merge pull request #444 from pi8027/fix-makefileCyril Cohen
Fix the doc-clean target of Makefile
2019-11-29Fix MakefileKazuhiko Sakaguchi
2019-11-28Merge pull request #439 from math-comp/CohenCyril-patch-1Cyril Cohen
remove duplicated sentence in CHANGELOG_UNRELEASED
2019-11-27Merge pull request #441 from ggonthier/big_enumCyril Cohen
Big enum
2019-11-27Explicit `bigop` enumeration handlingGeorges Gonthier
Added lemmas `big_enum_cond`, `big_enum` and `big_enumP` to handle more explicitly big ops iterating over explicit enumerations in a `finType`. The previous practice was to rely on the convertibility between `enum A` and `filter A (index_enum T)`, sometimes explicitly via the `filter_index_enum` equality, more often than not implicitly. Both are likely to fail after the integration of `finmap`, as the `choiceType` theory can’t guarantee that the order in selected enumerations is consistent. For this reason `big_enum` and the related (but currently unused) `big_image` lemmas are restricted to the abelian case. The `big_enumP` lemma can be used to handle enumerations in the non-abelian case, as explained in the `bigop.v` internal documentation. The Changelog entry enjoins clients to stop relying on either `filter_index_enum` and convertibility (though this PR still provides both), and warns about the restriction of the `big_image` lemma set to the abelian case, as it it a possible source of incompatibility.
2019-11-27Merge pull request #428 from maximedenes/build-docCyril Cohen
Add Makefile target to build the doc
2019-11-25Have to change directory before checking for the dependency fileYves Bertot
2019-11-25adds a comment so that dead code can be remove when it is no longer usedYves Bertot
2019-11-25dependency file will change name after coq-8.10Yves Bertot
2019-11-25things that are needed to make 'make doc' workYves Bertot
2019-11-25Add missing dependenciesMaxime Dénès
Spotted by Yves.
2019-11-25Add Makefile target to build the docMaxime Dénès
2019-11-25remove duplicated sentence in CHANGELOG_UNRELEASEDCyril Cohen
2019-11-24Merge pull request #438 from pi8027/hint-databaseCyril Cohen
Fix hint declarations to specify the database explicitly
2019-11-25Fix hint declarations to specify the database explicitlyKazuhiko Sakaguchi
2019-11-23Merge pull request #437 from pi8027/gitignore-vos-vokCyril Cohen
Add *.vos and *.vok to .gitignore
2019-11-22Add *.vos and *.vok to .gitignoreKazuhiko Sakaguchi
2019-11-22Injectivity lemmas in fintype (#426)Kazuhiko Sakaguchi
2019-11-22Added ssrfun theorem `inj_compr` (#432)Cyril Cohen
2019-11-22New generalised induction idiom (#434)Georges Gonthier
Replaced the legacy generalised induction idiom with a more robust one that does not rely on the `{-2}` numerical occurrence selector, using either new helper lemmas `ubnP` and `ltnSE` or a specific `nat` induction principle `ltn_ind`. Added (non-strict in)equality induction helper lemmas Added `ubnP[lg]?eq` helper lemmas that abstract an integer expression along with some (in)equality, in preparation for some generalised induction. Note that while `ubnPleq` is very similar to `ubnP` (indeed `ubnP M` is basically `ubnPleq M.+1`), `ubnPgeq` is used to remember that the inductive value remains below the initial one. Used the change log to give notice to users to update the generalised induction idioms in their proofs to one of the new forms before Mathcomp 1.11.
2019-11-20Merge pull request #399 from CohenCyril/ltn_subYves Bertot
More arithmetic theorems
2019-11-19Merge pull request #420 from pi8027/all-lemmasCyril Cohen
Add all_filter, all_pmap, and all_allpairsP in seq.v
2019-11-18fixing CHANGELOG and ltn_pred lemmasCyril Cohen
2019-11-18Documenting `L` and `R` in `CONTRIBUTING.md`Cyril Cohen
2019-11-18More arithmetic theoremsCyril Cohen
- Generalizing `ltn_subr` - Adding `ltn_subl` and `ltn_subr` - Changing conclusion of `ltn_predl` to `0 < n` instead of `n != 0`
2019-11-18Merge pull request #381 from hivert/seqYves Bertot
More lemmas on seqs
2019-11-15More lemmas on seqsFlorent Hivert
2019-11-15fix in ssralg (#421)Cyril Cohen
* missing exports of lemmas `commrB`, `commr_sum` and `commr_prod` * missing `regular_*` canonical exports
2019-11-15Add all_filter, all_pmap, and all_allpairsP in seq.vKazuhiko Sakaguchi
2019-11-14Merge pull request #423 from thery/docYves Bertot
typo
2019-11-14typothery
2019-11-14fingraph: remove fin_inj_bij lemma as duplicate of injF_bij from fintype (#403)Anton Trunov
2019-11-14Lemmas on commutation with big sum and prod (#413)Florent Hivert
* Lemmas on commutation with big sum and prod * Added commrB Lemma * @CohenCyril review * apply -> apply:
2019-11-14Update pull_request_template.mdCyril Cohen
2019-11-14Update zmodp.v (#411)Gabriel Taumaturgo
2019-11-14some information about naming conventions for definitions (wip) (#415)affeldt-aist
2019-11-14typo (#412)Laurent Théry
2019-11-06Merge pull request #410 from GTaumaturgo/patch-1Cyril Cohen
Update README.md
2019-11-06Merge pull request #408 from chdoc/existsPnCyril Cohen
add existsPn/forallPn lemmas
2019-11-06Merge pull request #406 from hivert/algebrasCyril Cohen
Commutative Algebras
2019-11-04Update README.mdGabriel Taumaturgo
2019-11-04Fixed the documentationFlorent Hivert
2019-11-04minor revisionChristian Doczkal
2019-11-04Fixed inheritance of fieldExt / fieldOver / splitting fieldFlorent Hivert
2019-11-04add existsPn/forallPn lemmasChristian Doczkal
2019-11-03Interface for commutative and commutative-unitary algebrasFlorent Hivert
Initial properties of polynomials in R-algebras
2019-10-31Merge pull request #378 from pi8027/fix-ltngtPCyril Cohen
Reorder the arguments in `compare_nat` and `ltngtP`
2019-10-30Change the order of arguments in `ltngtP`Kazuhiko Sakaguchi
from `ltngtP m n : compare_nat m n (m <= n) (n <= m) (m < n) (n < m) (n == m) (m == n)` to `ltngtP m n : compare_nat m n (n == m) (m == n) (n <= m) (m <= n) (n < m) (m < n)`, to make it tries to match subterms with `m < n` first, `m <= n`, then `m == n`.
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-06 04:57:07 +0000