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
/
finalg.v
Age
Commit message (
Expand
)
Author
2020-10-07
Turn class_of records into primitive records and get rid of the xclass idiom
Kazuhiko Sakaguchi
2019-12-28
Refactoring and linting especially polydiv
Kazuhiko Sakaguchi
2019-04-26
Cleaning Require and Require Imports
Cyril Cohen
2019-04-06
Fix inheritance bugs in finalg and extremal
Kazuhiko Sakaguchi
2019-04-02
Fix inheritances in countalg and finalg (the 2nd attempt)
Kazuhiko Sakaguchi
2019-03-19
Fix countalg to finalg inheritances
Kazuhiko Sakaguchi
2018-12-04
Remove `_ : Type` from packed classes
Anton Trunov
2018-10-26
moving countalg and closed_field around
Cyril Cohen
2018-02-21
Change Implicit Arguments to Arguments in algebra
Jasper Hugunin
2018-02-06
running semi-automated linting on the whole library
Cyril Cohen
2016-11-07
update copyright banner
Assia Mahboubi
2015-12-04
Correct join values to baseFingroupType
Georges Gonthier
2015-07-28
update copyright banner
Enrico Tassi
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-03-09
Initial commit
Enrico Tassi