coq-mathcomp - Library of mathematical components formalized in Coq

Age	Commit message (Collapse)	Author
2020-11-25	Rename `all1rel` to `all2rel`, restate `eq_allrel`, and add CHANGELOG entries	Kazuhiko Sakaguchi
	Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>
2020-11-25	Generalize `allrel` to take two lists as arguments	Kazuhiko Sakaguchi

2020-11-19	Removing duplicate clears and turning the warning into an error	Cyril Cohen

2020-10-30	Use `exp` rather than `X` for exponents of polynomials	Kazuhiko Sakaguchi

2020-10-29	Switch from long suffixes to short suffixes	Kazuhiko Sakaguchi

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-04-26	Cleaning Require and Require Imports	Cyril Cohen

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-04-16	[separable] put clear switch near view	Enrico
	Dear devs, in an attempt to simplify the code of intro patterns we came up with a proposal that: - simplifies the code of the plugin - breaks only one line in the entire mathcomp, the one fixed by this patch. The code we want to simplify is the one deferring clear switches inside an intro pattern. The implementation is tricky because just delaying the clear switch until the end of the pattern is not enough, for example: ``` move=> {x} /andP[x y]. ``` In this case `x` is both cleared and used. In order to be able to use `x`, given that the clear has not been performed yet, we rename `x` into `_x_` (when `{x}` is executed) so that when `x` is later executed we can use the name `x`, and then `.` is executed clear `_x_` instead of `x`. So systematically "always rename now & clear later" seem to be OK, but it is not. The extra complication is that "rename" may break later intro pattern using terms as views. Eg ``` move=> {x} /andP[Ha Hb] /x. ``` What the code does today is: - when `{x}` is execute look-ahead in the patter and see if `x` is used as a name to be introduced - if so, "rename" - otherwise don't rename (just delay) This way of doing things is not only complicated but also incomplete, Eg ``` move=> {x} /orP[x \| /x]. ``` would misbehave, since the look-ahead is not "semantic". Anyway, the proposed behavior is: - `{x}` always renames now and clears (the renamed) later - `{clears}/views` is always "compiled" as `/views{clears}` (most of the occurrences in the library are ok with this simpler rule, but for the one fixed in this PR). - bonus: support `{}/view` (as in `rewrite {}rule`) to signal that the immediately following `view` has to be cleared, that is `{}/v` compiled as `/v{v}`. What do you think? ``` ```
2018-02-21	Change Implicit Arguments to Arguments in field	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
	It was emitting a deprecation warning and will soon be removed from Coq.
2016-11-07	update copyright banner	Assia Mahboubi

2015-12-04	Remove spurious injections	Georges Gonthier

2015-07-28	update copyright banner	Enrico Tassi

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

2015-04-09	field for v8.5	Cyril Cohen

2015-03-09	Initial commit	Enrico Tassi