> BTW: I'm also considering dropping coqtop.byte and coqide.byte from the
> package on native archs since they are quite big, unless someone objects
> to it.
I do :-) From the Coq manual:
6.4.3 Declare ML Module string1 .. stringn.
This commands loads the Objective Caml compiled files string1 ...stringn
(dynamic link). It is mainly used to load tactics dynamically. The files are
searched into the current Objective Caml loadpath (see the command Add ML
Path in the section 6.5). Loading of Objective Caml files is only possible
under the bytecode version of coqtop (i.e. coqtop called with options -byte,
see chapter 12).
Cheers,
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]
