coq-mathcomp/mathcomp/fingroup, 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












Drop support for Coq 8.10 and deprecate the `deprecate` notation
2021-01-15T15:28:21+00:00

Kazuhiko Sakaguchi

2020-12-15T13:05:15+00:00

5f748f7ed9940c0db56e7dadd166f5e69bde6da9

- The `deprecate` notation and `iota_add` have been deprecated. All the uses of
  the `deprecate` notation have been replaced with the `deprecated` attribute.
- Deprecation aliases in `ssrnat` and `ssrnum` introduced in MathComp 1.11+beta1
  have been removed.
- Remove `VDFILE` related hacks from `Makefile.common`.





- The `deprecate` notation and `iota_add` have been deprecated. All the uses of
  the `deprecate` notation have been replaced with the `deprecated` attribute.
- Deprecation aliases in `ssrnat` and `ssrnum` introduced in MathComp 1.11+beta1
  have been removed.
- Remove `VDFILE` related hacks from `Makefile.common`.







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












Adding `permS01`
2020-11-02T14:23:56+00:00

Cyril Cohen

2020-04-05T18:04:22+00:00

486e08591c443093cdb602de7f603f84df72be42












Switch from long suffixes to short suffixes
2020-10-29T03:31:31+00:00

Kazuhiko Sakaguchi

2020-10-08T15:21:00+00:00

c6e0d703165b0c60c270672eb542aa8934929bfe












rename mem_imset2 to imset2_f (with deprecation)
2020-09-29T09:10:31+00:00

Christian Doczkal

2020-09-10T16:15:25+00:00

5b31a9e767694ce134fdff4461a876411eba0f2d












rename mem_imset to imset_f (with deprecation)
2020-09-29T09:10:31+00:00

Christian Doczkal

2020-09-10T15:45:57+00:00

298830c5a3860c7a645df6effe7d1cc228d56150












Putting ord1 in fintype
2020-09-27T13:09:15+00:00

Cyril Cohen

2020-04-10T09:45:05+00:00

4241f07301e8d84186ae2c80d5c32118a90f6847

ord1 is in zmodp, but it does not really require the zmodType structure of 'I_n to be stated and proven if we state it with ord0. We still keep the variant in zmodp with 0 instead of ord0 (for readability purposes).





ord1 is in zmodp, but it does not really require the zmodType structure of 'I_n to be stated and proven if we state it with ord0. We still keep the variant in zmodp with 0 instead of ord0 (for readability purposes).