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.