Coq-based packages

[Julien Puydt <julien.puydt@gmail.com>]

Hi,

I just changed the binary packages provided by the source coq package
to follow more closely upstream's subpackages. I used
Provides+Breaks+Replaces so things should go smoothly.

Now I would like to work on other things:

(1) the source package coq-doc (non-free) should be updated to latest
upstream, to follow more closely what we provide as coq ;

(2) the source package ssreflect provides libssreflect-coq ; in fact
it's packaging what upstream calls mathcomp, and should provide things
like libcoq-mathcomp-algebra, libcoq-mathcomp-character, libcoq-
mathcomp-field, libcoq-mathcomp-fingroup, libcoq-mathcomp-solvable and
libcoq-mathcomp-ssreflect (all with Breaks on libssreflect-coq) -- and
probably a libcoq-mathcomp depending on the previous list (with
Breaks+Provides+Replaces on libssreflect-coq).

(3) the source package mathcomp exists, and doesn't provide anything ;
in fact it was just imported two years ago in salsa from anonscm, and
didn't see any activity.

(4) I'll want to package https://github.com/math-comp/analysis (as
src:mathcomp-analysis providing libcoq-mathcomp-analysis)
[aside: that's the reason why above I propose the name libcoq-mathcomp
and not libcoq-mathcomp-all...]

For point (1), I think I can go ahead just now.

To deal with points (2) and (3), I'll definitely want the new
src:mathcomp and binary packages to derive from the current
src:ssreflect package, but for that some actions will have to be made
by team managers:

- salsa's mathcomp should be put out of the way (where?) ;

- salsa's ssreflect should be renamed to mathcomp.

Point (4) can wait until points (1)-(3) are done.

Does that plan sound ok?

Cheers,

J.Puydt