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
/
fingroup
/
gproduct.v
Age
Commit message (
Expand
)
Author
2020-11-19
Removing duplicate clears and turning the warning into an error
Cyril Cohen
2020-10-29
Switch from long suffixes to short suffixes
Kazuhiko Sakaguchi
2020-09-29
rename mem_imset2 to imset2_f (with deprecation)
Christian Doczkal
2019-11-27
Explicit `bigop` enumeration handling
Georges Gonthier
2019-11-22
New generalised induction idiom (#434)
Georges Gonthier
2019-05-17
refactor `seq` permutation theory
Georges Gonthier
2019-04-26
Cleaning Require and Require Imports
Cyril Cohen
2018-11-21
Merge Arguments and Prenex Implicits
Anton Trunov
2018-07-12
Replace all the CoInductives with Variants
Kazuhiko Sakaguchi
2018-03-04
Change deprecated Arguments Scope to Arguments
Jasper Hugunin
2018-02-21
Change Implicit Arguments to Arguments in fingroup
Jasper Hugunin
2018-02-06
running semi-automated linting on the whole library
Cyril Cohen
2017-10-30
Fix obsolete vernacular syntax for locality.
Maxime Dénès
2016-11-07
update copyright banner
Assia Mahboubi
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