| Age | Commit message (Collapse) | Author |
|---|
|
We chose to stick to the most general possible API, even though the macro
will not make full use of the possibilities. It makes explicit the various
data expected to be provided in an orthogonal way.
|
|
Unfortunately, mli-only files cannot be included in packs, so we have
the weird situation that the scope for `Tacexpr` is wrong. So we
cannot address the module as `Ltac_plugin.Tacexpr` but it lives in the
global namespace instead.
This creates problem when using other modular build/packing strategies
[such as #6857] This could be indeed considered a bug in the OCaml
compiler.
In order to remedy this situation we face two choices:
- leave the module out of the pack (!)
- create an implementation for the module
I chose the second solution as it seems to me like the most sensible
choice.
cc: #6512.
|
|
For now, a few vernacular features were lot in the process, like locating
Ltac definitions. This will be fixed in an upcoming commit.
|
|
In the previous setting, all plugins/ltac/*.cmxs except ltac_plugin.cmxs
(for instance coretactics.cmxs, g_auto.cmxs, ...) were utterly bogus :
- wrong -for-pack used for their inner .cmx
- dependency over modules not provided (for instance Tacenv, that ends
up being a submodule of the pack ltac_plugin).
But we were lucky, those files were actually never loaded, thanks to the
several DECLARE PLUGIN inside coretactics and co, that end up in ltac_plugin,
and hence tell Coq that these modules are already known, preventing
any attempt to load them.
Anyway, this commit cleans up this mess (thanks PMP for the help)
|
|
This reverts commit e8137ae63b3b19436755f372b595e7343e942894,
was meant for 8.6 branch only.
|
|
|
|
This is cumbersome, because now code may fail at link time if it's not
referring to the correct module name. Therefore, one has to add corresponding
open statements a the top of every file depending on a Ltac module. This
includes seemingly unrelated files that use EXTEND statements.
|
