coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| * \| \| \| \|	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#713: Bump year in headers.	Maxime Dénès	2017-06-15
\| \| \| \| \|\
\| \| \| \| * \	Merge PR#440: Univs: fix bug #5365, generation of u+k <= v constraints	Maxime Dénès	2017-06-15
\| \| \| \| \|\ \
\| \| \| \| * \ \	Merge PR#752: Adding a test case as requested in bug 5205.	Maxime Dénès	2017-06-15
\| \| \| \| \|\ \ \
\| \| \| \| * \ \ \	Merge PR#747: Fix Bug #5568, no dup notation warnings on repeated module imports	Maxime Dénès	2017-06-15
\| \| \| \| \|\ \ \ \
* \| \| \| \| \ \ \ \	Merge PR#719: Constrexpr.Numeral without bigint	Maxime Dénès	2017-06-15
\|\ \ \ \ \ \ \ \ \
\| \| \| \| * \| \| \| \| \|	plugins/ltac : avoid spurious .cmxs files	Pierre Letouzey	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
\| \|/ / / / / / / / \|/\| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \|	Fix Bug #5568, no dup notation warnings on repeated module imports	Paul Steckler	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
\|\ \ \ \ \ \ \ \ \| \| \|_\|/ / / / / \| \|/\| \| \| \| \| \|
\| \| \| \| \| * \| \|	Adding a test case as requested in bug 5205.	Théo Zimmermann	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
\|\ \ \ \ \ \ \ \
\| \| \| \| \| \| \| * \|	Univs: fix bug #5365, generation of u+k <= v constraints	Matthieu Sozeau	2017-06-05
* \| \| \| \| \| \| \| \|	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
\| \| \| \|/ / / / / / / / / /
\| \| \| \| \| \| \| \| \| \| \| \| *	Bump year in headers.	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
\| \| \| \| \| \| * \| \| \| \| \| \|	Merge PR#710: Add test-suite checks for coqchk with constraints	Maxime Dénès	2017-06-01
\| \| \| \| \| \| \|\ \ \ \ \ \ \ \| \| \| \| \| \| \| \|_\|/ / / / / \| \| \| \| \| \| \|/\| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR#704: Fix empty parentheses display in test-suite	Maxime Dénès	2017-06-01
\|\ \ \ \ \ \ \ \ \ \ \ \ \