coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	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.
*	STM: new worker for queries	Enrico Tassi	2014-10-31
	With the options -async-queries-always-delegate queries are always delegated to a worker process (Eval, Check, ...). Users of PIDE based UIs (in Denmark) reported that the current behavior of processing query synchronously is rather unexpected when one is used to get proofs processed asynchronously. Non instantaneous queries are part of many scripts and are there as "tests" for testing the execution of recursive functions. A standard proof script shape in an ongoing work by Appel and Bengtson is made of blocks like: - recursive function definition, - some tests, - some proofs And one cannot quickly jump over the tests (only the proofs). Enclosing the queries into dummy proofs to recover a reactive UI is just annoying. Hence this patch. Currently CoqIDE is not able to integrate the asynchronous feedback of the query workers into the document, hence if one passes the option to CoqIDE one only gets a boolean out of queries (processed/error).