Quentin VERMANDE
Quentin VERMANDE
Hello pPomCo. Thank you for the contribution. I will do a first review. Apart from a few specific comments (to come), the only issues I see are the spacing conventions...
It looks great (although is not the opam package `coq-mathcomp-classical`?). I believe the README here is more visible, so it should be documented here too.
Yes, here it is (I only need the contents of `engine/evd.ml`): https://github.com/Tragicus/coq/tree/utils For reference, I opened a PR for this branch: https://github.com/coq/coq/pull/18820
It was long ago so I might be mistaken, but I am pretty sure this solved our issue back then. I can do the benchmarking tomorrow.
I can compile neither `master` nor `coq-master` neither on coq's `master` nor `v8.19`. Can you tell me which branches I should take?
Here it is: ``` Raised at Exninfo.iraise in file "clib/exninfo.ml", line 79, characters 4-11 Called from Evarconv.conv_record.(fun) in file "pretyping/evarconv.ml", line 1190, characters 21-50 Called from Stdlib__List.fold_left in file "list.ml",...
It did not change anything.
Lines 714-811 contain the roots-coefficients relations for a polynomial. Should it go to mathcomp or should I put it in the xmathcomp directory (or have I just not seen it...
In fact, what I did is not complete. I proved that any extension that is solvable by radical is solvable in any characteristic, but not the converse, so AbelGalois still...
I managed to do it using (essentially) the decidability of equality between elements of the galois group. I have quite a few auxiliary lemmas, that I have temporarily put in...