coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	STM: Print/Extraction have to be skipped if -quick	Enrico Tassi	2016-02-19
	Print and Extraction commands may pierce opacity: if the task producing the proof term is not finished, we wait for its completion. In -quick mode no worker is going to process a task, since tasks are simply stored to disk (and resumed later in -vio2vo mode). This commit avoids coqc waits forever for a task in order to Print/Extract the corresponding term. Bug reported privately by Alec Faithfull.