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
2018-10-31
fixing local Makefile
Cyril Cohen
2018-10-29
Revert "Adding allsigs, the dependent version of allpairs"
Cyril Cohen
2018-10-29
Merge pull request #219 from CohenCyril/Makefile
Enrico
2018-10-26
Merge pull request #235 from CohenCyril/bool_irrelevance2
Cyril Cohen
2018-10-26
fix some bugs in Makefile
Cyril Cohen
2018-10-26
Statement of `bool_irrelevance` more consistent with its name.
Cyril Cohen
2018-10-26
moving countalg and closed_field around
Cyril Cohen
2018-10-26
removing multiple definitions of [tT]ag*
Cyril Cohen
2018-10-25
Merge pull request #232 from anton-trunov/master
Enrico
2018-10-24
Adding allsigs, the dependent version of allpairs
Cyril Cohen
2018-10-03
[opam]: add dev-repo links
Anton Trunov
2018-09-24
Implementation of all2 (#224)
Pierre-Yves Strub
2018-09-13
Small scale tool for proving "the following are equivalent"
Cyril Cohen
2018-09-11
Fixes the doc of rat
Florent Hivert
2018-09-04
[warnings] -w "+compatibility-notation" clean
Enrico Tassi
2018-08-06
changing companionmx to a more standard one
Cyril Cohen
2018-08-03
update ChangeLog and doc
Cyril Cohen
2018-08-01
Companion matrix of a polynomial
Cyril Cohen
2018-08-01
simplified, cleaned and documented Makefile.common
Cyril Cohen
2018-07-31
agressive fix for duplicated files!
Cyril Cohen
2018-07-31
change coqdep
Cyril Cohen
2018-07-31
some things should always be done
Cyril Cohen
2018-07-31
removing dead code + reshuffling stuff
Cyril Cohen
2018-07-31
Rework the whole Makefile architecture
Cyril Cohen
2018-07-24
Add addnBAC, addnBCA, and addnABC lemmas to ssrnat
Anton Trunov
2018-07-19
Merge pull request #202 from CohenCyril/improving-poly
Laurent Théry
2018-07-19
last_eq for exhaustivity
Cyril Cohen
2018-07-19
poly_size_eq1 phrased with reflect + combinators
Cyril Cohen
2018-07-14
updated proposition for big_prod_seq_eq1
Cyril Cohen
2018-07-14
Laurent's simplifications
Cyril Cohen
2018-07-12
Replace all the CoInductives with Variants
Kazuhiko Sakaguchi
2018-07-04
small generalizations in poly
Cyril Cohen
2018-04-24
fix opam packager script + dependencies
Cyril Cohen
2018-04-20
fix symlinks to README, INSTALL and LICENSE
Enrico Tassi
2018-04-20
remove the attic/ directory
Enrico Tassi
2018-04-20
remove ssr plugin for 8.4 and 8.5
Enrico Tassi
2018-04-20
Fix the script that generates the doc
Enrico Tassi
2018-04-20
remove v8.4 code from Makefile
Enrico Tassi
2018-04-20
Merge remote-tracking branch 'origin/pr/189'
Enrico Tassi
2018-04-20
Merge remote-tracking branch 'origin/pr/192'
Enrico Tassi
2018-04-20
Merge remote-tracking branch 'origin/pr/191'
Enrico Tassi
2018-04-20
Merge remote-tracking branch 'origin/pr/193'
Enrico Tassi
2018-04-18
Moving real_closed to another repo
Cyril Cohen
2018-04-17
Removing undocumented compatibility module
Cyril Cohen
2018-04-17
move odd_order to its own repository
Enrico Tassi
2018-04-16
[separable] put clear switch near view
Enrico
2018-04-12
ssrnat: don't use `fix n` but rather `fix name n`
Enrico Tassi
2018-04-12
remove ssrtest: it now belongs to Coq
Enrico Tassi
2018-03-21
Declare prenex implicits for `Some_inj`
Anton Trunov
2018-03-20
Merge pull request #185 from jashug/deprecate-arguments-scope
Enrico
[next]