coq-mathcomp - Library of mathematical components formalized in Coq

Age	Commit message (Collapse)	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

2020-09-29	rename mem_imset to imset_f (with deprecation)	Christian Doczkal

2019-11-22	New generalised induction idiom (#434)	Georges Gonthier
	Replaced the legacy generalised induction idiom with a more robust one that does not rely on the `{-2}` numerical occurrence selector, using either new helper lemmas `ubnP` and `ltnSE` or a specific `nat` induction principle `ltn_ind`. Added (non-strict in)equality induction helper lemmas Added `ubnP[lg]?eq` helper lemmas that abstract an integer expression along with some (in)equality, in preparation for some generalised induction. Note that while `ubnPleq` is very similar to `ubnP` (indeed `ubnP M` is basically `ubnPleq M.+1`), `ubnPgeq` is used to remember that the inductive value remains below the initial one. Used the change log to give notice to users to update the generalised induction idioms in their proofs to one of the new forms before Mathcomp 1.11.
2019-05-29	Replace eqVneq with eqPsym	Anton Trunov
	Also changed eqsVneq.
2019-04-26	Cleaning Require and Require Imports	Cyril Cohen

2018-12-04	Document parameter names whenever possible	Anton Trunov
	As suggested by @ggonthier [here](https://github.com/math-comp/math-comp/pull/249#pullrequestreview-177938295) > One of the design ideas for the `Arguments` command was that it would allow to centralise the documentation of the application of constants. In that spirit it would be in my opinion better to make as much use of this as possible, and to document the parameter names whenever possible, especially that of implicit parameters. and [here](https://github.com/math-comp/math-comp/pull/253#discussion_r237434163): > As a general rule, defined functional constants should have maximal prenex implicit arguments, as this facilitates their use as arguments to functionals, because this mimics the way function constants are treated in functional programming languages with Hindley-Milner type inference. Conversely, lemmas and theorems should have on-demand implicit arguments, possibly interspersed with explicit ones, as it's fairly common for other lemmas to have universally quantified premises; also, this makes it easier to specify such arguments with the apply: tactic. This policy may be amended for lemmas that are used as functional arguments, such as reflection or cancellation lemmas. Unfortunately there is currently no easy way to tell Coq to use different defaults for definitions and lemmas, so MathComp sticks to the on-demand default, as there are significantly more lemmas than definition, and use the Prenex Implicits to redress matters in bulk for definitions. However, this is not completely systematic, and is sometimes omitted for constants that are not used as functional arguments in the library, or inside the sections in which the definition occur, since such commands need to be repeated after the section is closed. Since Arguments commands should document the intended constant usage as best as possible, they should follow the implicits policy - even in cases such as this where the Prenex Implicits had been skipped.
2018-11-21	Merge Arguments and Prenex Implicits	Anton Trunov
	See the discussion here: https://github.com/math-comp/math-comp/pull/242#discussion_r233778114
2018-03-04	Change deprecated Arguments Scope to Arguments	Jasper Hugunin

2018-02-21	Change Implicit Arguments to Arguments in solvable	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	Removed spurious injection & clean up proof	Georges Gonthier

2015-07-28	update copyright banner	Enrico Tassi

2015-07-17	Updating files + reorganizing everything	Cyril Cohen

2015-04-09	adapting solvable to 8.5	Cyril Cohen

2015-03-09	Initial commit	Enrico Tassi