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
/
algebra
Age
Commit message (
Expand
)
Author
2017-02-04
adding rquot_comRingType
Cyril Cohen
2016-11-17
Merge remote-tracking branch 'upstream/master' into fixdoc
Florent Hivert
2016-11-16
Fixes the doc of mxalgebra
Florent Hivert
2016-11-07
update copyright banner
Assia Mahboubi
2016-10-24
wip shorter proof dec factor theorems
Cyril Cohen
2016-08-25
Factor theorem for decidable fields, (inspired by PY Strub)
Cyril Cohen
2016-08-25
Enriched numClosedFieldType so that it factors a lot of theory from both comp...
Cyril Cohen
2016-03-15
Merge pull request #34 from strub/master
Enrico
2016-03-15
all_algebra now exports zmodp
Pierre-Yves Strub
2016-02-06
typo in int divn1 -> divz1
thery
2015-12-12
switch ":" to "-"
Cyril Cohen
2015-12-04
Add finLmodType, finLalgType and finAlgType instances
Georges Gonthier
2015-12-04
Remove more redundant power type structures
Georges Gonthier
2015-12-04
Correct join values to baseFingroupType
Georges Gonthier
2015-12-04
Add missing export
Georges Gonthier
2015-11-10
fix INSTALL symlinks
Enrico Tassi
2015-07-28
update copyright banner
Enrico Tassi
2015-07-22
forgotten import
Cyril Cohen
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
Using the From X Require Y for v8.4
Cyril Cohen
2015-04-08
packaging for v8.5
Cyril Cohen
2015-04-08
makefiles that are version dependent
Cyril Cohen
2015-03-19
packaging fingroup and algebra
Cyril Cohen
2015-03-09
Initial commit
Enrico Tassi