Julien Puydt

Well, I just know that when several license assignments apply to the same file (from the main LICENSE file, from the top of the file itself and from below in...

Well, unless this [bug report](https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=1004461) misinterpreted the error log, you now have your first time.

I haven't tested your patch yet, but I asked around how to do it and was pointed to [a different diagnosis](https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=952740) for the issue.

Well, it works here, and prepending DESTDIR is what is usually done...

Here is another: ``` Section MissingRoot2. Variable R: fieldType. Lemma root_deg1 (a b r: R): a != 0 -> root (a *: 'X - b%:P) r = (r == b...

I like your proofs better, indeed. I'll try to name my branches in the future.

Ubuntu derives from Debian, so installing the libssreflect-coq package (which is math-comp) should trigger the installation of a corresponding version of coq ; and installing the coqide package should give...

I see it with coq 8.12.0 and math-comp 1.12.0.

I proposed flint/arb/ because I feared arb/ could be too short... Yes, that definitely breaks backwards compatibility (sagemath will have to cope with it).

Aren't filenames with a '-' looking for trouble? Notice that with a pkgconfig file, there would be no backwards compatibility breakage...