coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Improving e11854569b8 on when to print goals in coqtop mode.	Hugo Herbelin	2014-12-07
*	Trying a new policy for when to automatically print goals (granting	Hugo Herbelin	2014-12-04
*	fix compilation on ocaml 3.12 (Close: 3833)	Enrico Tassi	2014-11-28
*	STM: if a-p-always-delegate fetch states from parked worker on edit-at	Enrico Tassi	2014-11-28
*	STM: hook called whenever a state is unreachable	Enrico Tassi	2014-11-27
*	async_queries_* merged with async_proofs_*	Enrico Tassi	2014-11-27
*	AsyncTaskQueue: parsin can also happen in the workers now	Enrico Tassi	2014-11-27
*	STM: new API async_query	Enrico Tassi	2014-11-27
*	AsyncTaskQueue: API to park a worker	Enrico Tassi	2014-11-27
*	WorkerPool: API to move a worker from an active pool to a parking one	Enrico Tassi	2014-11-27
*	TQueue: let reader be picky when popping an item	Enrico Tassi	2014-11-27
*	STM: put hooks in key events to let plugins customize the feedback	Enrico Tassi	2014-11-27
*	Feedback: API cleaned up, documented and made user extensible	Enrico Tassi	2014-11-27
*	new: Optimize Proof, Optimize Heap	Enrico Tassi	2014-11-09
*	vernac_classifier: VernacDeclareTacticDefinition does not alter the parser	Enrico Tassi	2014-11-03
*	STM: code refactoring	Enrico Tassi	2014-11-03
*	STM: fix printing of goals when on a tty interface	Enrico Tassi	2014-11-03
*	Fix error reporting id on VtUnknown commands	Enrico Tassi	2014-11-03
*	Add [Info] command.	Arnaud Spiwack	2014-11-01
*	Feedback message: hold extra info to help routing	Enrico Tassi	2014-10-31
*	STM: new worker for queries	Enrico Tassi	2014-10-31
*	STM: reorganize code and file names	Enrico Tassi	2014-10-31
*	Fix backtracking issue in Defined (Close 3780)	Enrico Tassi	2014-10-30
*	Fixes for PG (Close 3763, 3770)	Enrico Tassi	2014-10-27
*	This commit introduces changes in induction and destruct.	Hugo Herbelin	2014-10-25
*	Goal printing made uniform: always done in STM (close 3585)	Enrico Tassi	2014-10-22
*	Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.	Arnaud Spiwack	2014-10-22
*	Goal: remove most of the API (make [Goal.goal] concrete).	Arnaud Spiwack	2014-10-16
*	Fix -async-proofs-always-delegate (close 3740)	Enrico Tassi	2014-10-15
*	Stm: more precise representation of nested proofs	Enrico Tassi	2014-10-13
*	STM: primitives to snapshot a .vi while in interactive mode	Enrico Tassi	2014-10-13
*	TQueue: new primitive to take a snapshot of the queue	Enrico Tassi	2014-10-13
*	STM: simplify how the term part of a side effect is retrieved	Enrico Tassi	2014-10-13
*	library/opaqueTables: enable their use in interactive mode	Enrico Tassi	2014-10-13
*	STM: report the (structured) goals as XML	Carst Tankink	2014-10-01
*	Add additional location information to AST XMLs.	Carst Tankink	2014-10-01
*	Add syntax for naming new goals in refine: writing ?[id] instead of _	Hugo Herbelin	2014-09-30
*	XML pretty printing for AST (work by François Poulain, project DoCoq)	Enrico Tassi	2014-09-29
*	Notation: option to attach extra pretty printing rules to notations	Enrico Tassi	2014-09-29
*	Undo prints only if coqtop \|\| emacs	Enrico Tassi	2014-09-16
*	Uniformisation of the order of arguments env and sigma.	Hugo Herbelin	2014-09-12
*	VernacExtend does not dispatch on type anymore.	Pierre-Marie Pédrot	2014-09-10
*	Marshalling errors should be bold and red (should never happen actually)	Enrico Tassi	2014-09-09
*	A marshalling failure does not make a worker `Old	Enrico Tassi	2014-09-09
*	Back: print subgoals as in 8.4 (Close: 3585)	Enrico Tassi	2014-09-09
*	BackTo not part of the doc when used by emacs	Enrico Tassi	2014-09-09
*	Undo: if the ui is coqtop (command line) then Undo is not part of the doc.	Enrico Tassi	2014-09-09
*	Dropped proofs (Abort) are evaluated synchronously (Closes: 3550, 3407)	Enrico Tassi	2014-09-09
*	Remove [Infer] option of records.	Arnaud Spiwack	2014-09-04
*	Print [Variant] types with the keyword [Variant].	Arnaud Spiwack	2014-09-04