The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Mon, Oct 14, 2013 at 09:55:45PM +0200, Thomas Braibant wrote:
> Hi,
> 
> > I also expect to see more and more Coq developments relying on existing
> > plugins (ssreflect, mtac,...) or combinations thereof, so the idea you
> > mentioned of having persistent packages is probably worth exploring.
> 
> Yes, I have the same feeling. Note though that mtac is a patch of Coq,
> not a plugin (even if it may change in the future, afaik), and
> therefore, lives in its own switch. I would really like to know if
> there are other packages like ssreflect 1) that takes a long time to
> compile, 2) people often switch from version to version.

Just for the records, from version 1.5 ssreflect and the mathematical
components library will split.  Ssreflect will contain "only" the files
up to and including fintype.  This takes way less time to compile than
the whole math comp library.

Still there are users of the whole library ;-)

Ciao
-- 
Enrico Tassi