index
:
coq-mathcomp
master
Library of mathematical components formalized in Coq
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
mathcomp
Age
Commit message (
Expand
)
Author
2020-06-06
General theory of min and max, and use in ssrnum
Cyril Cohen
2020-06-06
Increasing definitional equalities
Cyril Cohen
2020-06-06
Generalizing max and min to porderType
Cyril Cohen
2020-06-05
Merge pull request #514 from affeldt-aist/lemmas_from_analysis_20200521
Yves Bertot
2020-06-05
fix naming
Reynald Affeldt
2020-06-05
Missing mono lemmas (#513)
Cyril Cohen
2020-06-04
fix naming
Reynald Affeldt
2020-06-03
add real_* variants
Reynald Affeldt
2020-06-02
another lemma about norm from mathcomp-analysis
Reynald Affeldt
2020-05-22
tentative change of naming convention and add variants
Reynald Affeldt
2020-05-21
three lemmas that we found useful in the context of the
Reynald Affeldt
2020-05-16
A few more revisions
Kazuhiko Sakaguchi
2020-05-13
Revise proofs in ssreflect/*.v
Kazuhiko Sakaguchi
2020-05-04
Merge pull request #493 from pi8027/rm-tuple-lemmas-in-order
Cyril Cohen
2020-05-04
Remove the tuple extensions in order.v that is available in tuple.v
Kazuhiko Sakaguchi
2020-04-21
Add dual_finLatticeType and fix dual_finDistrLatticeType
Kazuhiko Sakaguchi
2020-04-15
reworked new lemmas in perm and action and added missing ones
Cyril Cohen
2020-04-15
addressing comments about PR#221 of mathcomp
Reynald Affeldt
2020-04-15
Some more lemmas on permutations
Florent Hivert
2020-04-15
Merge pull request #475 from CohenCyril/ssrnat_deprecated_symbols
affeldt-aist
2020-04-10
adding depreciations in ssrnat
Cyril Cohen
2020-04-10
adding guard conditions check to the test_suite
Cyril Cohen
2020-04-10
Make `all2` better wrt the guard condition
Cyril Cohen
2020-04-09
Merge pull request #473 from affeldt-aist/long_short_suffixes
affeldt-aist
2020-04-09
Merge pull request #431 from ppedrot/rm-constr-hint-decls
affeldt-aist
2020-04-09
- switching long suffixes to short suffixes
Reynald Affeldt
2020-04-09
Merge pull request #474 from llelf/doc-typos
affeldt-aist
2020-04-09
docs: more ".-tuple" fixes
Antonio Nikishaev
2020-04-09
more typos
Antonio Nikishaev
2020-04-09
Update mathcomp/ssreflect/ssrnat.v
Antonio Nikishaev
2020-04-08
fix typos in documentation: formulae
Antonio Nikishaev
2020-04-08
fix typos in documentation: text
Antonio Nikishaev
2020-04-07
Merge pull request #211 from CohenCyril/ssrAC
Enrico Tassi
2020-04-08
Remove hint declarations using non-global definitions.
Pierre-Marie Pédrot
2020-04-06
Some proof scripts made better using ssrAC.
Cyril Cohen
2020-04-06
Rewriting with AC (not modulo AC), using a small scale command.
Cyril Cohen
2020-04-06
minor documentation fix
Reynald Affeldt
2020-04-02
Merge pull request #468 from ybertot/remove-deprecated-from-1.9
Enrico Tassi
2020-04-01
Merge pull request #429 from pi8027/extend-nat-comparison
Yves Bertot
2020-03-31
remove deprecated commands whose deprecation was introduced in release 1.9.0
Yves Bertot
2020-03-31
Merge pull request #457 from CohenCyril/find
Yves Bertot
2020-03-16
Update mathcomp/ssreflect/path.v
Cyril Cohen
2020-03-16
Link between subrelations and path/sorted
Cyril Cohen
2020-03-15
just noticed a tentative use of a not yet existing lemma
Reynald Affeldt
2020-03-15
Reorder arguments of comparison predicates in order.v as they should
Kazuhiko Sakaguchi
2020-03-15
Extend comparison predicates for nat with minn and maxn
Kazuhiko Sakaguchi
2020-01-30
Merge pull request #453 from pi8027/experiment/order-nondistr-lattice
Pierre-Yves Strub
2020-01-29
Documentation work for (non-distributive) latticeType
Kazuhiko Sakaguchi
2020-01-28
Added lemmas about foldl, scanl, foldr and rcons and cons
Cyril Cohen
2020-01-28
Theorems about find and index
Cyril Cohen
[next]