coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR#787: [typeclasses eauto] Fix bug #3943: non-termination in topological	Maxime Dénès	2017-06-19
\|\
* \	Merge PR#760: Fixing base_include after loc is an option + a better test that...	Maxime Dénès	2017-06-19
\|\ \
* \ \	Merge PR#613: Cumulativity for inductive types	Maxime Dénès	2017-06-19
\|\ \ \
* \| \| \|	Test case for bug 5578.	Maxime Dénès	2017-06-19
* \| \| \|	Increase the time limit on 4366.v to make gitlab work better.	Gaëtan Gilbert	2017-06-16
\| * \| \|	Fix a bug in cumulativity	Amin Timany	2017-06-16
\| * \| \|	Clean up universes of constants and inductives	Amin Timany	2017-06-16
\| * \| \|	Move (part of) tests from checker to success	Amin Timany	2017-06-16
\| * \| \|	Checker add test for non-trivial constraints	Amin Timany	2017-06-16
\| * \| \|	Change the option to Set Inductive Cumulativity	Amin Timany	2017-06-16
\| * \| \|	Correct coqchk reduction	Amin Timany	2017-06-16
\| * \| \|	Disable debug printing	Amin Timany	2017-06-16
\| * \| \|	Fix bugs and add an option for cumulativity	Amin Timany	2017-06-16
\| * \| \|	Fix bugs	Amin Timany	2017-06-16
\|/ / /
* \| \|	Merge PR#719: Constrexpr.Numeral without bigint	Maxime Dénès	2017-06-15
\|\ \ \
* \ \ \	Merge PR#375: Deprecation	Maxime Dénès	2017-06-15
\|\ \ \ \
* \| \| \| \|	Remove dependency on -compat flag in coq_makefile test suite.	Maxime Dénès	2017-06-15
* \| \| \| \|	Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").	Maxime Dénès	2017-06-14
\|\ \ \ \ \
\| \| \| \| \| *	[typeclasses eauto] Fix bug #3943: non-termination in topological	Matthieu Sozeau	2017-06-14
* \| \| \| \| \|	Prelude : no more autoload of plugins extraction and recdef	Pierre Letouzey	2017-06-14
\| \| \| * \| \|	Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)	Pierre Letouzey	2017-06-14
\| \|_\|/ / / \|/\| \| \| \|
\| \| * \| \|	Remove support for Coq 8.4.	Guillaume Melquiond	2017-06-14
\| \|/ / / \|/\| \| \|
* \| \| \|	Merge PR#498: Bignums as a separate opam package	Maxime Dénès	2017-06-14
\|\ \ \ \
* \ \ \ \	Merge PR#385: Equality of sigma types	Maxime Dénès	2017-06-13
\|\ \ \ \ \ \| \|_\|_\|_\|/ \|/\| \| \| \|
* \| \| \| \|	Merge PR#757: Better sectioning on travis log printing in test-suite	Maxime Dénès	2017-06-13
\|\ \ \ \ \
\| \| \| * \| \|	BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)	Pierre Letouzey	2017-06-13
\| \|_\|/ / / \|/\| \| \| \|
* \| \| \| \|	Merge PR#709: Bytecode compilation apart from 'make world', again	Maxime Dénès	2017-06-12
\|\ \ \ \ \
* \| \| \| \| \|	Add support for "-bypass-API" argument of "coq_makefile"	Matej Košík	2017-06-12
* \| \| \| \| \|	make test-suite/save-logs.sh usable also on old MacOS X	Maxime Denes	2017-06-12
\| \| \| \| \| *	A stronger test that #use"include";; works well.	Hugo Herbelin	2017-06-11
\| \|_\|_\|_\|/ \|/\| \| \| \|
\| \| * \| \|	Fix Travis sectioning	Jason Gross	2017-06-10
\| \| * \| \|	Better sectioning on travis log printing in test-suite	Jason Gross	2017-06-09
\| \|/ / / \|/\| \| \|
\| \| \| *	A fix to #5414 (ident bound by ltac names now known for "match").	Hugo Herbelin	2017-06-09
\| \|_\|/ \|/\| \|
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-06-08
\|\ \ \
* \ \ \	Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a sh...	Maxime Dénès	2017-06-06
\|\ \ \ \
* \ \ \ \	Merge PR#600: Some factorizations of ltac interpretation functions between ss...	Maxime Dénès	2017-06-06
\|\ \ \ \ \
* \| \| \| \| \|	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
* \| \| \| \| \|	Merge PR#691: [travis] Add OSX test-suite checking.	Maxime Dénès	2017-06-02
\|\ \ \ \ \ \
\| \| \| \| * \ \	Merge PR#705: Fix bug #5019 (looping zify on dependent types)	Maxime Dénès	2017-06-02
\| \| \| \| \|\ \ \
* \| \| \| \| \ \ \	Merge PR#647: [emacs] [toplevel] Make emacs flag local to the toplevel.	Maxime Dénès	2017-06-02
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR#711: [gitlab] Artifact test suite logs on failure.	Maxime Dénès	2017-06-02
\|\ \ \ \ \ \ \ \ \
\| \| \| * \| \| \| \| \| \|	Test-suite: do not test native compiler if disabled by configure.	Maxime Dénès	2017-06-01
\| \| \| \| \| \| \| \| * \|	test-suite/coq-makefile: we do not build byte file by default anymore	Pierre Letouzey	2017-06-01
* \| \| \| \| \| \| \| \| \|	Merge PR#449: make specialize smarter (bug 5370).	Maxime Dénès	2017-06-01
\|\ \ \ \ \ \ \ \ \ \
\| \| \| * \| \| \| \| \| \| \|	[emacs] [toplevel] Make emacs flag local to the toplevel.	Emilio Jesus Gallego Arias	2017-06-01
\| \| \| \| \| \| \| * \| \| \|	Merge PR#631: Fix bug #5255	Maxime Dénès	2017-06-01
\| \| \| \| \| \| \| \|\ \ \ \
\| \| \| \| * \| \| \| \| \| \| \|	Fix coq_makefile uninstall target under OSX.	Maxime Dénès	2017-06-01
\| \| \| \|/ / / / / / / /
* \| \| \| \| \| \| \| \| \| \|	Merge PR#694: Fixing #5523 (missing support for complex constructions in recu...	Maxime Dénès	2017-06-01
\|\ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \| \|	Fix bug #5019 (looping zify on dependent types)	Jason Gross	2017-06-01
\| \| \| \| \| \| \| \| * \| \|	Add opened bug 5019	Jason Gross	2017-06-01