> - 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: [EMAIL PROTECTED] http://www.cs.unibo.it/~sacerdot ---------------------------------------------------------------- -- To UNSUBSCRIBE, email to [EMAIL PROTECTED] with a subject of "unsubscribe". Trouble? Contact [EMAIL PROTECTED]