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












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

Cyril Cohen

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

532de9b68384a114c6534a0736ed024c900447f9












packaging fingroup and algebra
2015-03-19T14:51:00+00:00

Cyril Cohen

2015-03-19T14:51:00+00:00

0d2a1e7388d45776700c4400781e1aa71a0f0060

The files zmodp and cyclic in fingroup had dependecies in algebra so I put them there.
I'm not convinced it's the best solution to this problem.
Maybe more subdivisions in algebra would bring a better solution?

(Maybe we should send the whole problem to a solver? :P)





The files zmodp and cyclic in fingroup had dependecies in algebra so I put them there.
I'm not convinced it's the best solution to this problem.
Maybe more subdivisions in algebra would bring a better solution?

(Maybe we should send the whole problem to a solver? :P)