coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Change references to CAMLP4 to CAMLP5 to be more accurate since we no	Jim Fehrle	2018-02-17
\| \| \| \|	longer use camlp4.
*	[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
\|
*	Remove the Sigma (monotonous state) API.	Maxime Dénès	2017-06-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Reminder of (some of) the reasons for removal: - Despite the claim in sigma.mli, it does not prevent evar leaks, something like: fun env evd -> let (evd',ev) = new_evar env evd in (evd,ev) will typecheck even with Sigma-like type annotations (with a proof of reflexivity) - The API stayed embryonic. Even typing functions were not ported to Sigma. - Some unsafe combinators (Unsafe.tclEVARS) were replaced with slightly less unsafe ones (e.g. s_enter), but those ones were not marked unsafe at all (despite still being so). - There was no good story for higher order functions manipulating evar maps. Without higher order, one can most of the time get away with reusing the same name for the updated evar map. - Most of the code doing complex things with evar maps was using unsafe casts to sigma. This code should be fixed, but this is an orthogonal issue. Of course, this was showing a nice and elegant use of GADTs, but the cost/benefit ratio in practice did not seem good.
*	Exporting a few primitive tacticals as named Ltac definitions.	Pierre-Marie Pédrot	2017-05-27
\|
*	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
\| \| \| \|	Now it is a private field, locations are optional.
*	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.