aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/solvable/burnside_app.v
AgeCommit message (Expand)Author
2019-10-30Change the order of arguments in `ltngtP`Kazuhiko Sakaguchi
2019-05-29Replace eqVneq with eqPsymAnton Trunov
2019-05-29Rename eqsP to eqPsym as suggested by @CohenCyrilAnton Trunov
2019-05-28Add eqsP view to destruct not only x == y, but also y == xAnton Trunov
2019-04-26Cleaning Require and Require ImportsCyril Cohen
2019-04-01Compatibility fix for Coq issue coq/#9663Georges Gonthier
2019-04-01Making {fun ...} structural and extending it to dependent functionsGeorges Gonthier
2018-12-04Document parameter names whenever possibleAnton Trunov
2018-02-21Change Implicit Arguments to Arguments in solvableJasper Hugunin
2018-02-06fixing things that @ggonthier and @ybertot spotted and some I spottedCyril Cohen
2018-02-06running semi-automated linting on the whole libraryCyril Cohen
2016-11-07update copyright bannerAssia Mahboubi
2015-07-28update copyright bannerEnrico Tassi
2015-07-17Updating files + reorganizing everythingCyril Cohen
2015-04-09adapting solvable to 8.5Cyril Cohen
2015-03-09Initial commitEnrico Tassi