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
/
solvable
Age
Commit message (
Collapse
)
Author
2016-10-24
better ltngtP
Cyril Cohen
2015-12-12
switch ":" to "-"
Cyril Cohen
2015-12-04
Add elementary abelian finite modules lemmas to abelian
Georges Gonthier
This factors proofs in mxabelem and finfield and removes dependencies between these two files.
2015-12-04
Removed spurious injection & clean up proof
Georges Gonthier
2015-11-10
fix INSTALL symlinks
Enrico Tassi
2015-07-28
update copyright banner
Enrico Tassi
2015-07-22
remove duplicate fields
Cyril Cohen
2015-07-22
make the opam package meta data
Cyril Cohen
2015-07-21
update opam meta-data
Cyril Cohen
2015-07-18
update to preserve backward compatibility with v8.4
Cyril Cohen
2015-07-17
Updating files + reorganizing everything
Cyril Cohen
2015-04-09
adapting solvable to 8.5
Cyril Cohen
2015-04-09
Using the From X Require Y for v8.4
Cyril Cohen
2015-04-08
makefiles that are version dependent
Cyril Cohen
2015-03-24
change finfield from field to character
Cyril Cohen
2015-03-24
metadata for solvable and field
Cyril Cohen
2015-03-09
Initial commit
Enrico Tassi
[prev]