coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Being more informative about the change of behavior of "subst".	Hugo Herbelin	2016-09-29
*	fix bug 3683 : adds references to the web site for the bug tracker	Yves Bertot	2016-09-29
*	Fix bug #5011: Anomaly on [Existing Class].	Pierre-Marie Pédrot	2016-09-29
*	test-suite: fix sed on OS X, does not handle +	Matthieu Sozeau	2016-09-29
*	Ncring_initial: avoid a notation overriding	Pierre Letouzey	2016-09-29
*	Extraction: ignore some useless stuff about universes	Pierre Letouzey	2016-09-29
*	Argument : assert does fail if no arg is given (fix #4864)	Enrico Tassi	2016-09-29
*	-profile-ltac-cutoff alike Show Ltac Profile Cutoff (#5100)	Enrico Tassi	2016-09-29
*	Ring_theory: avoid overriding a few notations	Pierre Letouzey	2016-09-28
*	ZDivEucl: notations in different scope to avoid a warning	Pierre Letouzey	2016-09-28
*	Adding interface files to Nsatz ML files.	Pierre-Marie Pédrot	2016-09-28
*	Do not stop propagation of signals when Coq is busy (bug #3941).	Guillaume Melquiond	2016-09-28
*	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