coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \|	Adding variants enter_one and refine_one which assume that exactly one	Hugo Herbelin	2016-09-16
* \| \|	Added a test file for contradiction.	Hugo Herbelin	2016-09-15
* \| \|	Extending "contradiction" so that it recognizes statements such as "~x=x" or ...	Hugo Herbelin	2016-09-15
* \| \|	Continuing fix to #5078, taking also into account intropatterns.	Hugo Herbelin	2016-09-15
* \| \|	Typo.	Hugo Herbelin	2016-09-15
* \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-14
\|\\| \|
\| * \|	Fixing test-suite after commit 43104a0b.	Pierre-Marie Pédrot	2016-09-14
* \| \|	Fixing #5078 (wrong detection of evaluable local hypotheses).	Hugo Herbelin	2016-09-13
* \| \|	LtacProp: fix reset_profile (fix #5079)	Enrico Tassi	2016-09-13
* \| \|	test-suite/output-modulo-time made more robust	Enrico Tassi	2016-09-13
* \| \|	AsyncTaskQueue: annotate debug feedback messages with worker id	Enrico Tassi	2016-09-13
* \| \|	CoqIDE: push to message win feedback Message(Debug,Info,Notice)	Enrico Tassi	2016-09-13
* \| \|	coqc: print debug feedback coming from workers	Enrico Tassi	2016-09-13
* \| \|	stm: feedback forwarding has to be atomic	Enrico Tassi	2016-09-13
* \| \|	feedback: provide a feeder that prints debug messages	Enrico Tassi	2016-09-13
\| * \|	Fixing a recursive notation bug raised on coq-club on Sep 12, 2016.	Hugo Herbelin	2016-09-12
* \| \|	Refolding: disable in 8.4 compat file, document	Matthieu Sozeau	2016-09-12
* \| \|	Merge remote-tracking branch 'github-coq/pr/249' into v8.6	Matthieu Sozeau	2016-09-12
\|\ \ \
* \| \| \|	Add support for testing output mod timing changes	Jason Gross	2016-09-11
* \| \| \|	Fix newlines in printout of LtacProf	Jason Gross	2016-09-11
* \| \| \|	Revert the LtacProf tactic table header	Jason Gross	2016-09-11
* \| \| \|	Add a test for 4836	Jason Gross	2016-09-11
* \| \| \|	Avoid putting a useless "toploop" directory in the ML search path if it does ...	Guillaume Melquiond	2016-09-10
\| \| * \|	Test for #5077.	Hugo Herbelin	2016-09-10
\| \| * \|	Fixing #5077 (failure on typing a fixpoint with evars in its type).	Hugo Herbelin	2016-09-10
* \| \| \|	Updating .gitignore.	Hugo Herbelin	2016-09-09
\| * \| \|	no-refold patch	Paul Steckler	2016-09-09
* \| \| \|	Fix output test-suite after commit 0d3c319.	Pierre-Marie Pédrot	2016-09-09
* \| \| \|	Fast path in Clenvtac.clenv_refine typeclass resolution.	Pierre-Marie Pédrot	2016-09-09
* \| \| \|	Monomorphize a costly boolean equality operation.	Pierre-Marie Pédrot	2016-09-09
* \| \| \|	Fix bug #4940: Tactic notation printing could be more informative.	Pierre-Marie Pédrot	2016-09-09
* \| \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-09
\|\ \ \ \ \| \|/ / / \|/\| / / \| \|/ /
\| * \|	Restore native compiler optimizations after they were broken by 9e2ee58.	Maxime Dénès	2016-09-09
* \| \|	Make it explicit when paths are added to the ML search paths.	Guillaume Melquiond	2016-09-09
* \| \|	Update csdp cache.	Pierre-Marie Pédrot	2016-09-09
* \| \|	Fix bug #3920 for good after 44ada64.	Pierre-Marie Pédrot	2016-09-09
* \| \|	Fix Bug #5073 : regression of micromega plugin	Frédéric Besson	2016-09-08
* \| \|	Avoid canonizing the same paths over and over.	Guillaume Melquiond	2016-09-08
* \| \|	Fix Bug #5073 : regression of micromega plugin	Frédéric Besson	2016-09-08
* \| \|	Merge PR #271 into v8.6	Pierre-Marie Pédrot	2016-09-08
\|\ \ \
\| * \| \|	Fix a typo in the reference manual	Jason Gross	2016-09-07
\|/ / /
* \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-07
\|\\| \|
* \| \|	CoqIDE: Errors are sticky (fix #4368)	Enrico Tassi	2016-09-07
* \| \|	Removing useless tactic compatibility layer in Rewrite.	Pierre-Marie Pédrot	2016-09-07
* \| \|	STM: if_verbose on "Checking task ..." (fix #4058)	Enrico Tassi	2016-09-07
* \| \|	ltacprof: rec-calls are coaleshed	Enrico Tassi	2016-09-07
* \| \|	micromega : more robust generation of proof terms	Frédéric Besson	2016-09-07
* \| \|	A proposal to unify the messages given by Test and Print Options (#5062).	Hugo Herbelin	2016-09-06
* \| \|	STM: queries give back a dummy safe_id in case of error (#5041)	Enrico Tassi	2016-09-06
* \| \|	STM: sideff: report safe_id correctly (fix #4968)	Enrico Tassi	2016-09-06