Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Make most of TACTIC EXTEND macros runtime calls. | 2018-03-08 | |
| | | | | | | | | | Today, TACTIC EXTEND generates ad-hoc ML code that registers the tactic and its parsing rule. Instead, we make it generate a typed AST that is passed to the parser and a generic tactic execution routine. PMP has written a small parser that can generate the same typed ASTs without relying on camlp5, which is overkill for such simple macros. | ||
* | Update headers following #6543. | 2018-02-27 | |
| | |||
* | Change references to CAMLP4 to CAMLP5 to be more accurate since we no | 2018-02-17 | |
| | | | | longer use camlp4. | ||
* | [API] Remove `open API` in ml files in favor of `-open API` flag. | 2017-07-17 | |
| | |||
* | Bump year in headers. | 2017-07-04 | |
| | |||
* | plugins/ltac : avoid spurious .cmxs files | 2017-06-15 | |
| | | | | | | | | | | | | | | 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) | ||
* | Remove (useless) aliases from the API. | 2017-06-10 | |
| | |||
* | Put all plugins behind an "API". | 2017-06-07 | |
| | |||
* | Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFun | 2017-03-14 | |
| | |||
* | Ltac as a plugin. | 2017-02-17 | |
This commit is essentially moving files around. In particular, the corresponding plugin still relies on a mllib file rather than a mlpack one. Otherwise, this causes link-time issues for third-party plugins depending on modules defined in the Ltac plugin. |