coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Warning about similar notations now up to alpha-conversion.	Hugo Herbelin	2016-09-28
*	Typeclass backtracking example by J. Leivant	Matthieu Sozeau	2016-09-28
*	Remove incorrect assertion in cbn (bug #4822).	Guillaume Melquiond	2016-09-28
*	Merge remote-tracking branch 'github/pr/232' into v8.6	Maxime Dénès	2016-09-28
\|\
* \|	Fix bug #4553: CoqIDE gives warnings about deprecated GTK features.	Pierre-Marie Pédrot	2016-09-27
* \|	Fix #5061: Warnings flag has no discernible value	Maxime Dénès	2016-09-27
* \|	Add fixed test-suite file for bug #4527	Matthieu Sozeau	2016-09-27
* \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-27
\|\ \
* \| \|	LtacProf: "Show Ltac Profile CutOff $N" (fix #5080)	Enrico Tassi	2016-09-27
* \| \|	Remove spaces from around list notations	Jason Gross	2016-09-26
* \| \|	Remove spaces from around vector notations	Jason Gross	2016-09-26
* \| \|	Unbreak Ltac [ \| .. \| ] notation in -compat 8.5	Jason Gross	2016-09-26
* \| \|	Fix bug #4785 (use [ ] for vector nil)	Jason Gross	2016-09-26
* \| \|	Posssible abstractions over goal variables when inferring match return clause.	Hugo Herbelin	2016-09-26
* \| \|	Trying an abstracting dependencies heuristic for the match return clause even...	Hugo Herbelin	2016-09-26
* \| \|	Trying a no-inversion no-dependency heuristic for match return clause.	Hugo Herbelin	2016-09-26
* \| \|	Inference of return clause: giving uniformly priority to "small inversion".	Hugo Herbelin	2016-09-26
* \| \|	Fast russian peasant exponentiation in Nsatz.	Pierre-Marie Pédrot	2016-09-26
* \| \|	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
\| * \|	Ensuring that the evar name is preserved by "rename" as it is already	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