coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias	2017-07-17
\|
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	plugins/ltac : avoid spurious .cmxs files	Pierre Letouzey	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.	Matej Košík	2017-06-10
\|
*	Put all plugins behind an "API".	Matej Kosik	2017-06-07
\|
*	Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFun	Maxime Dénès	2017-03-14
\|
*	Ltac as a plugin.	Pierre-Marie Pédrot	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.