coq - The formal proof system

Age	Commit message (Collapse)	Author
2018-07-02	Moving various ml4 files to mlg.	Pierre-Marie Pédrot

2018-03-08	Make most of TACTIC EXTEND macros runtime calls.	Maxime Dénès
	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.
2018-02-27	Update headers following #6543.	Théo Zimmermann

2018-02-17	Change references to CAMLP4 to CAMLP5 to be more accurate since we no	Jim Fehrle
	longer use camlp4.
2017-07-17	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias

2017-07-04	Bump year in headers.	Pierre-Marie Pédrot

2017-06-15	plugins/ltac : avoid spurious .cmxs files	Pierre Letouzey
	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)
2017-06-10	Remove (useless) aliases from the API.	Matej Košík

2017-06-07	Put all plugins behind an "API".	Matej Kosik

2017-03-14	Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFun	Maxime Dénès

2017-02-17	Ltac as a plugin.	Pierre-Marie Pédrot
	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.