Re: [Fwd: R?sum? discussion licence de Coq]
> - Oh, and it's twice the size of the old one even without the IDE.
That's because of {theories,states,contrib}7.
> (Do the theories7, states7 and contrib7 directories really need to be
> there for users working on new theories? Should they go in a
> separate package? coqtop bombs if called with the -translate option
> if they don't exist. _Seems_ to work otherwise. OTOH, its only
> 5.5Mb)
They are required only for -translate and not for new developments.
Nevertheless -translate is necessary to users with old contribs.
Maybe the best option is to make a second Coq package with just
the {..,..,..}7 stuff.
> Don't know if the bit about pcoq contradicts this - it didn't
> translate very well :o(
No, it doesn't.
Hope it helps,
C.S.C.
--
----------------------------------------------------------------
Real name: Claudio Sacerdoti Coen
Doctor in Computer Science, University of Bologna
E-mail: sacerdot@cs.unibo.it
http://www.cs.unibo.it/~sacerdot
----------------------------------------------------------------
Reply to: