Re: Processing of coq_8.0pl2-1_i386.changes
> 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: sacerdot@cs.unibo.it
http://www.cs.unibo.it/~sacerdot
----------------------------------------------------------------
Reply to: