coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fix FIXME: use OCaml 4.02 generative functors when available.	Gaëtan Gilbert	2017-11-01
\| \| \| \|	4.02.3 has been the minimal OCaml version for a while now.
*	[stm] Switch to a functional API	Emilio Jesus Gallego Arias	2017-10-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	We make the Stm API functional over an opaque `doc` type. This allows to have a much better picture of what the toplevel is doing; now almost all users of STM private data are marked by typing. For now only, the API is functional; a PR switching the internals should come soon thou; however we must first fix some initialization bugs. Due to some users, we modify `feedback` internally to include a "document id" field; we don't expose this change in the IDE protocol yet.
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	[stm] Add common toploop for workers.	Emilio Jesus Gallego Arias	2017-03-21
\| \| \| \| \|	This is a small, but convenient refactoring, as it will allow common argument parsing.
*	Update copyright headers.	Maxime Dénès	2016-01-20
\|
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	STM: code refactoring	Enrico Tassi	2014-11-03
\| \| \| \| \|	This is mainly shuffling code around and removing internal refs that are not needed anymore.
*	coqworkmgr	Enrico Tassi	2014-09-02
\|
*	STM: new "par:" goal selector, like "all:" but in parallel	Enrico Tassi	2014-08-05
	par: distributes the goals among a number of workers given by -async-proofs-tac-j (defaults to 2).