coq-mathcomp/mathcomp/_CoqProject, branch master Library of mathematical components formalized in Coq Silencing warning deprecated-ident-entry 2021-03-12T21:45:02+00:00 Cyril Cohen 2021-03-04T21:45:19+00:00 be445d437200da5765c972074dd0c0de68562adc 






Silence Hint Locality warning
2021-03-04T21:56:43+00:00

Cyril Cohen

2021-03-04T21:56:43+00:00

081c7c29feb1f4c2e66331a88c273f802c9bc27c












Removing duplicate clears and turning the warning into an error
2020-11-19T20:38:46+00:00

Cyril Cohen

2020-11-19T17:33:21+00:00

e565f8d9bebd4fd681c34086d5448dbaebc11976












add declare scopes
2020-11-19T11:39:55+00:00

Reynald Affeldt

2020-11-19T10:18:39+00:00

c83609826d97afda6b11b227207f461cf077a0d5












Turn class_of records into primitive records and get rid of the xclass idiom
2020-10-07T14:23:26+00:00

Kazuhiko Sakaguchi

2020-09-10T12:19:55+00:00

ad55cb4128382852370ea53d36f4d21a83274e8b












refactor `seq` permutation theory
2019-05-17T07:04:50+00:00

Georges Gonthier

2019-05-08T07:43:34+00:00

5d7bd2ea2a0a28fb275da8ba2e2c0dc5a33d1034

- Change the naming of permutation lemmas so they conform to a
consistent policy: `perm_eq` lemmas have a `perm_` (_not_ `perm_eq`)
prefix, or sometimes a `_perm` suffix for lemmas that _prove_ `perm_eq`
using a property when there is also a lemma _using_ `perm_eq` for the
same property. Lemmas that do not concern `perm_eq` do _not_ have
`perm` in their name.
- Change the definition of `permutations` for a time- and space-
back-to-front generation algorithm.
- Add frequency tally operations `tally`, `incr_tally`, `wf_tally` and
`tally_seq`, used by the improved `permutation` algorithm.
- add deprecated aliases for renamed lemmas





- Change the naming of permutation lemmas so they conform to a
consistent policy: `perm_eq` lemmas have a `perm_` (_not_ `perm_eq`)
prefix, or sometimes a `_perm` suffix for lemmas that _prove_ `perm_eq`
using a property when there is also a lemma _using_ `perm_eq` for the
same property. Lemmas that do not concern `perm_eq` do _not_ have
`perm` in their name.
- Change the definition of `permutations` for a time- and space-
back-to-front generation algorithm.
- Add frequency tally operations `tally`, `incr_tally`, `wf_tally` and
`tally_seq`, used by the improved `permutation` algorithm.
- add deprecated aliases for renamed lemmas







we silence warnings that just pollute our logs (#275)
2019-02-05T14:42:11+00:00

Enrico

2019-02-05T14:42:11+00:00

5ba21e9d4a2ec934f09dc316603df83eee345d41

Namely:
-projection-no-head-constant
-redundant-canonical-projection
-notation-overridden




Namely:
-projection-no-head-constant
-redundant-canonical-projection
-notation-overridden






Broken global Makefile
2015-04-02T11:31:52+00:00

Cyril Cohen

2015-04-02T11:31:52+00:00

e2530e78deda5cf6be2111951efb8ea747af7fa8