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












silencing warnings in individual packages
2020-06-08T13:11:01+00:00

Cyril Cohen

2020-06-08T13:11:01+00:00

fe6a6d967a8613695fde95f1652a8fa56c4b5d28












moving countalg and closed_field around
2018-10-26T01:33:07+00:00

Cyril Cohen

2018-07-28T19:30:02+00:00

bccc54dc85e2d9cd7248c24a576d6092630fb51d

- countalg goes to the algebra package
- finalg now get the expected inheritance from countalg
- closed_field now contains the construction of algebraic closure for countable fields (previously in countalg)
- proof of quantifier elimination for closed field rewritten in a monadic style





- countalg goes to the algebra package
- finalg now get the expected inheritance from countalg
- closed_field now contains the construction of algebraic closure for countable fields (previously in countalg)
- proof of quantifier elimination for closed field rewritten in a monadic style







Move finfield to field module
2015-12-04T15:07:20+00:00

Georges Gonthier

2015-12-01T17:45:46+00:00

37f0673c5ecaf1325095f06f1eb8b1478313e5b1












Updating files + reorganizing everything
2015-07-17T16:03:31+00:00

Cyril Cohen

2015-07-17T16:03:31+00:00

532de9b68384a114c6534a0736ed024c900447f9












change finfield from field to character
2015-03-24T14:07:18+00:00

Cyril Cohen

2015-03-24T14:07:18+00:00

f3671d37b31f0745a82e6968157bfbb0c0c959e9












metadata for solvable and field
2015-03-24T11:23:33+00:00

Cyril Cohen

2015-03-24T11:23:33+00:00

c7ddacdfc43ba25c9fbd9505b3960047c13596d0