coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Fixing Coq compilation.	Pierre-Marie Pédrot	2014-11-26
*	Experimenting always forcing convertibility on strict implicit arguments	Hugo Herbelin	2014-11-26
*	Registering strict implicit arguments systematically.	Hugo Herbelin	2014-11-26
*	Bug #3804 is actually closed (thanks to Jason Gross for the notification).	Xavier Clerc	2014-11-25
*	Tweak some test cases.	Xavier Clerc	2014-11-25
*	Fix order of arguments in Extract Constant for Pos.compare_cont.	Maxime Dénès	2014-11-25
*	Adding tag output to references in Ppconstr.	Pierre-Marie Pédrot	2014-11-25
*	Used an evar name based on the local def name in "evar" tactic.	Hugo Herbelin	2014-11-25
*	A bit more information in debug tactic unification.	Hugo Herbelin	2014-11-25
*	Adapting to current semantics of "simpl non-evaluable-cst"	Hugo Herbelin	2014-11-25
*	Experimenting using unification when matching evar/meta free subterms	Hugo Herbelin	2014-11-25
*	Plugging console highlighting in for toplevel and compilation error messages.	Pierre-Marie Pédrot	2014-11-24
*	Adding test for bug #3248.	Pierre-Marie Pédrot	2014-11-24
*	Fixing bug #3817.	Pierre-Marie Pédrot	2014-11-24
*	Pass around information on the use of template polymorphism for	Matthieu Sozeau	2014-11-23
*	One more word about "simpl f": avoid "simpl f" to be printed "simpl f",	Hugo Herbelin	2014-11-23
*	Add printer for transparent state for ocamldebug.	Hugo Herbelin	2014-11-23
*	Partly revert commit d9681fb94a3e04a618e58cd09df9cee929170edc about	Hugo Herbelin	2014-11-23
*	Fix #3824. de Bruijn error in normalization of fixpoints.	Maxime Dénès	2014-11-23
*	Specific printer of Evar.Set.t for ocamldebug + more information in	Hugo Herbelin	2014-11-22
*	Attempt to organize and document unification flags of setoid rewrite.	Hugo Herbelin	2014-11-22
*	Removing superfluous newlines in setoid_rewrite error message.	Hugo Herbelin	2014-11-22
*	In setoid_rewrite error messages:	Hugo Herbelin	2014-11-22
*	Test for closed #2713 and #2876.	Hugo Herbelin	2014-11-22
*	Further simplifying functional induction.	Hugo Herbelin	2014-11-22
*	Simplifying code of functional induction.	Hugo Herbelin	2014-11-22
*	Not using an (arbitrary) pivot anymore for re-introduction of	Hugo Herbelin	2014-11-22
*	New simplification of code for generalizing hypotheses in destruct.	Hugo Herbelin	2014-11-22
*	Removing a hack which, according to the comment, should not be necessary	Hugo Herbelin	2014-11-22
*	Add test-suite file for dependent rewriting example by Vadim Zaliva and	Matthieu Sozeau	2014-11-22
*	Fix resolve_morphism to build well-scoped terms in case some arguments	Matthieu Sozeau	2014-11-22
*	Enforcing the non-normalization of evars in Tactics.get_next_hyp_position.	Pierre-Marie Pédrot	2014-11-22
*	Writing intro_replacing in the new monad.	Pierre-Marie Pédrot	2014-11-22
*	Removing useless flag of the historical move tactic.	Pierre-Marie Pédrot	2014-11-22
*	Exporting a primitive allowing to run completely the tactic monad.	Pierre-Marie Pédrot	2014-11-22
*	Adding test for bug #3326.	Pierre-Marie Pédrot	2014-11-21
*	Adding test for bug #3424.	Pierre-Marie Pédrot	2014-11-21
*	Cleaning up closed bugs in test-suite.	Pierre-Marie Pédrot	2014-11-21
*	Writing Tactics.keep in the new monad.	Pierre-Marie Pédrot	2014-11-21
*	Test for bug #3788.	Pierre-Marie Pédrot	2014-11-21
*	Add test-suite file for bug #3804.	Matthieu Sozeau	2014-11-21
*	Fix bug #3804.	Matthieu Sozeau	2014-11-21