coq-mathcomp/mathcomp/character, 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`.







Merge pull request #667 from CohenCyril/ssrcoq8.10
2020-11-23T12:39:15+00:00

Enrico Tassi

2020-11-23T12:39:15+00:00

e6a25b8d4806cf968dbf6c33343ba1d1fb28ddf6

Using Coq 8.10 ssreflect new features




Using Coq 8.10 ssreflect new features






Using Coq 8.10 ssreflect new features
2020-11-20T11:10:46+00:00

Cyril Cohen

2020-11-19T19:37:16+00:00

1c03fed9bd5ab57b99405802f17d50ff0888f887












Merge pull request #663 from CohenCyril/clean_head
2020-11-20T08:55:19+00:00

affeldt-aist

2020-11-20T08:55:19+00:00

b4cdd47bcd7f2b2f9033ee00b7412570b07b8808

Using Arguments / to deal with volatile definitions




Using Arguments / to deal with volatile definitions






Using Arguments / to deal with volatile definitions
2020-11-20T02:10:59+00:00

Cyril Cohen

2020-11-20T02:10:59+00:00

7c47bab45686e90ee50e6c7eaae3230cb7ce9e53












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












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

Kazuhiko Sakaguchi

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

c6e0d703165b0c60c270672eb542aa8934929bfe