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












Rename `all1rel` to `all2rel`, restate `eq_allrel`, and add CHANGELOG entries
2020-11-25T13:29:55+00:00

Kazuhiko Sakaguchi

2020-11-25T13:14:58+00:00

d844896e6418bb00418964bb4ae4219e2bd6b69c

Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>





Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>







Generalize `allrel` to take two lists as arguments
2020-11-25T13:29:54+00:00

Kazuhiko Sakaguchi

2020-11-20T07:52:52+00:00

783631c771ec76baa4ff9d292c1eddfb58f67f4c












Tuning simplifications using Arguments simpl nomatch
2020-11-20T19:50:44+00:00

Cyril Cohen

2020-11-20T01:31:40+00:00

c55acd1fefa970cc4ed3a8a53b05fd77008a7cdf












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












Use `exp` rather than `X` for exponents of polynomials
2020-10-30T03:12:26+00:00

Kazuhiko Sakaguchi

2020-10-30T03:12:26+00:00

bd02346e4038871f4d4021dd84df384fc8cf9aa4












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

Kazuhiko Sakaguchi

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

c6e0d703165b0c60c270672eb542aa8934929bfe












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