coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Monomorphizing various uses of arrays in Nsatz.	Pierre-Marie Pédrot	2016-09-26
*	Partial fix for bug #5085: nsatz_compute stack overflows.	Pierre-Marie Pédrot	2016-09-26
*	Fix bug #5093: typeclasses eauto depth arg does not accept a var.	Pierre-Marie Pédrot	2016-09-26
*	Fix bug #5090: Effect of -Q depends on coqtop's current directory.	Pierre-Marie Pédrot	2016-09-25
*	The coqtop options -Q and -R do not affect the ML loadpath anymore.	Pierre-Marie Pédrot	2016-09-25
*	Moving "move" in the new proof engine.	Hugo Herbelin	2016-09-24
*	Adding a test for bug #5096.	Pierre-Marie Pédrot	2016-09-24
*	Fix bug #5096: [vm_compute] is exponentially slower than [native_compute].	Pierre-Marie Pédrot	2016-09-23
*	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-23
\|\
* \|	coqc -o now places .glob file near .vo file	Enrico Tassi	2016-09-22
* \|	typos	Enrico Tassi	2016-09-22
\| *	Fixing #5095 (non relevant too strict test in let-in abstraction).	Hugo Herbelin	2016-09-22
* \|	Fix description of change in intro semantics.	Maxime Dénès	2016-09-21
* \|	Remove dead code in library/lib.ml.	Maxime Dénès	2016-09-20
\| *	Replace { command ; } with ( command )	Erik Martin-Dorel	2016-09-19
\| *	Fix typos in RefMan-uti.tex.	Erik Martin-Dorel	2016-09-19
* \|	Fix warning when using Variables at toplevel.	Maxime Dénès	2016-09-19
* \|	Further "decide equality" tests on demand of Jason.	Hugo Herbelin	2016-09-17
* \|	Addressing OCaml compilation warnings.	Hugo Herbelin	2016-09-16
* \|	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