coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
\|\
* \|	Prelude : no more autoload of plugins extraction and recdef	Pierre Letouzey	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
\| \| * \| \|	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
\| \| \| \| \| \| * \| \| \| \|	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
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR#701: [readlink -f] doesn't work on OSX	Maxime Dénès	2017-05-31
\|\ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| * \| \| \| \| \| \| \|	[travis] print failing test suite logs on failure	Gaëtan Gilbert	2017-05-31
\| \| \| \| \| \| \| \| * \| \| \| \|	Merge PR#560: Reinstate fixpoint refolding in [cbn], deactivated by mistake (...	Maxime Dénès	2017-05-31
\| \| \| \| \| \| \| \| \|\ \ \ \ \
\| \| \| \| * \| \| \| \| \| \| \| \| \|	Tests for new specialize feature + CHANGES.	Pierre Courtieu	2017-05-31
\| \| \| \| \| \|_\|_\|_\|_\|_\|_\|/ / \| \| \| \| \|/\| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \| \| \| \|	Merge PR#699: Fix bug 5550: "typeclasses eauto with" does not work with secti...	Maxime Dénès	2017-05-31
\| \| \| \| \| \| \| \| \|\ \ \ \ \
\| \| \| \| \| \| * \| \| \| \| \| \| \|	Factorizing interp_gen through a function interpreting glob_constr.	Hugo Herbelin	2017-05-31
\| \| \| \| \| \|/ / / / / / / / \| \| \| \| \|/\| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \| \| \| \|	More precise on preventing clash between bound vars name and hidden impargs.	Hugo Herbelin	2017-05-31
\| \| \| \| \| \| * \| \| \| \| \| \|	Fixing #5233 (missing implicit arguments for recursive records).	Hugo Herbelin	2017-05-31
\| \| \| \| \| \| * \| \| \| \| \| \|	Fixing a failure to interpret some local implicit arguments in Inductive.	Hugo Herbelin	2017-05-31
\| \| \| \| \| \|/ / / / / / / \| \| \| \| \|/\| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \| \|	Fixing #5523 (missing support for complex constructions in recursive notations).	Hugo Herbelin	2017-05-31
\| \| \| * \| \| \| \| \| \| \| \|	Fixing a too lax constraint for finding recursive binder part of a notation.	Hugo Herbelin	2017-05-31
\| \| \| \|/ / / / / / / /
\| \| \| \| * / / / / / /	[gitlab] Artifact test suite logs on failure.	Gaëtan Gilbert	2017-05-30
\| \| \| \|/ / / / / / /
\| \| \| \| \| \| \| * / /	Add test-suite checks for coqchk with constraints	Jason Gross	2017-05-30
\| \| \| \| \| \|_\|/ / / \| \| \| \| \|/\| \| \| \|
\| \| * \| / \| \| \| \|	Fix empty parentheses display in test-suite	Jason Gross	2017-05-30
\| \| \|/ / / / / /
\| \| \| * \| \| \| \|	Merge PR#693: A subtle bug in tclWITHHOLES.	Maxime Dénès	2017-05-30
\| \| \| \|\ \ \ \ \
\| * \| \| \| \| \| \| \|	[readlink -f] doesn't work on OSX	Gaëtan Gilbert	2017-05-30
\| \|/ / / / / / /
* \| \| \| \| \| \| \|	Support for using type information to infer more precise evar sources.	Hugo Herbelin	2017-05-30
* \| \| \| \| \| \| \|	Few tests for e-variants of assert, set, remember.	Hugo Herbelin	2017-05-30
\|/ / / / / / /