coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|
*	Change references to CAMLP4 to CAMLP5 to be more accurate since we no	Jim Fehrle	2018-02-17
\| \| \| \|	longer use camlp4.
*	Add named timers to LtacProf	Jason Gross	2017-12-14
\| \| \| \| \| \| \| \| \| \|	I'm not sure if they belong in profile_ltac, or in extratactics, or, perhaps, in a separate plugin. But I'd find it very useful to have a version of `time` that works on constr evaluation, which is what this commit provides. I'm not sure that I've picked good naming conventions for the tactics, either.
*	Add tactics to reset and display the Ltac profile	Jason Gross	2017-12-14
\| \| \| \| \|	This is useful for tactics that run a bunch of tests and need to display the profile for each of them.
*	Allow LtacProf tactics to be called	Jason Gross	2017-12-11
\| \| \| \| \| \|	This fixes #6378. Previously the ML module was never declared anywhere. Thanks to @cmangin for the pointer.
*	[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
\|
*	Put all plugins behind an "API".	Matej Kosik	2017-06-07
\|
*	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.