coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge PR #6898: [compat] Remove "Intuition Iff Unfolding"	Maxime Dénès	2018-03-06
\|\
\| *	[compat] Remove "Intuition Iff Unfolding"	Emilio Jesus Gallego Arias	2018-03-03
\| \| \| \| \| \| \| \|	Following up on #6791, we remove the option "Intuition Iff Unfolding"
* \|	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|/
*	[ast] Improve precision of Ast location recognition in serialization.	Emilio Jesus Gallego Arias	2018-02-22
\| \| \| \| \| \| \| \| \|	We follow the suggestions in #402 and turn uses of `Loc.located` in `vernac` into `CAst.t`. The impact should be low as this change mostly affects top-level vernaculars. With this change, we are even closer to automatically map a text document to its AST in a programmatic way.
*	[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
\|
*	Merge PR#794: Cleanup of ltac cmxs	Maxime Dénès	2017-06-23
\|\
\| *	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)
* \|	Deprecate options that were introduced for compatibility with 8.2.	Guillaume Melquiond	2017-06-14
\| \|
* \|	Remove support for Coq 8.2.	Guillaume Melquiond	2017-06-14
\|/
*	Remove (useless) aliases from the API.	Matej Košík	2017-06-10
\|
*	Put all plugins behind an "API".	Matej Kosik	2017-06-07
\|
*	Ltac cleanup: no more constr_of_global calls	Matthieu Sozeau	2017-05-29
\|
*	Merge PR#481: [option] Remove support for non-synchronous options.	Maxime Dénès	2017-05-25
\|\
* \	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\ \
\| \| *	[option] Remove support for non-synchronous options.	Emilio Jesus Gallego Arias	2017-05-24
\| \|/ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which this PR solves, I propose to remove support for non-synchronous options. It seems the few uses of `optsync = false` we legacy and shouldn't have any impact. Moreover, non synchronous options may create particularly tricky situations as for instance, they won't be propagated to workers.
\| *	Fix 4.04 warnings	Gaetan Gilbert	2017-04-27
\| \|
\| *	Add [_] prefix to unused values which maybe should be kept	Gaetan Gilbert	2017-04-27
\| \|
* \|	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
\| \| \| \| \| \| \| \|	Now it is a private field, locations are optional.
* \|	[location] Use located in tactics.	Emilio Jesus Gallego Arias	2017-04-24
\|/ \| \| \|	One case missing due the TACTIC EXTEND macro.
*	Merge branch 'trunk' into pr379	Maxime Dénès	2017-03-24
\|
*	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.