Adding the possibility for ML modules to declare functions to be called at
caching time, i.e. when the Declare ML Module command is evaluated. This can
be used by both static and dynamic plugins.
Plugin names must be declared in the header of .ml4 file, be they static or
dynamic. This is done with the "DECLARE PLUGIN \"name\"" macro.
Moving the ML tactic extension mechanism to a Libobject-based one.
Now parsing rules of ML-declared tactics are only made available after the
corresponding Declare ML Module command. This changes essentially two
things:

1. ML plugins are forced to use the DECLARE PLUGIN statement before any
TACTIC EXTEND statement. The plugin name must be exactly the string passed to
the Declare ML Module command.

2. ML tactics are only made available after the Coq module that does the
corresponding Declare ML Module is imported. This may break a few things,
as it already broke quite some uses of omega in the stdlib.