coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix coqdoc test-suite target on Windows.	Théo Zimmermann	2017-08-21
*	Merge PR #942: solving b1859	Maxime Dénès	2017-08-16
\|\
* \	Merge PR #954: Print names of all open blocks	Maxime Dénès	2017-08-16
\|\ \
* \ \	Merge PR #841: Timorous fix of bug #5598 on global existing class in sections	Maxime Dénès	2017-08-16
\|\ \ \
* \ \ \	Merge PR #880: Fix coqdoc bug #5648 on user idents colliding with keywords wr...	Maxime Dénès	2017-08-16
\|\ \ \ \
* \ \ \ \	Merge PR #864: Some cleanups after cumulativity for inductive types	Maxime Dénès	2017-08-16
\|\ \ \ \ \
\| \| \| \| \| *	Adding a test for BZ#1859 as suggested by @tchajed.	Théo Zimmermann	2017-08-15
\| \| \| \| * \|	Print names of all open blocks	Tej Chajed	2017-08-06
\| \|_\|_\|/ / \|/\| \| \| \|
* \| \| \| \|	Merge PR #928: Fixing bug #5671 (tactic specialize unclean wrt Metas).	Maxime Dénès	2017-08-01
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #926: test-suite uses Extraction TestCompile	Maxime Dénès	2017-08-01
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #909: Extraction: reduce primitive projections in types (fix bug 4709)	Maxime Dénès	2017-08-01
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #834: Adding support for recursive notations of the form "x , .. , y...	Maxime Dénès	2017-08-01
\|\ \ \ \ \ \ \ \
\| \| \| \| \| * \| \| \|	Change the option for cumulativity	Amin Timany	2017-07-31
\| \| \| \| \| * \| \| \|	Add Jason's example of fun-ext with cumulativity	Amin Timany	2017-07-31
\| \| \| \| \| * \| \| \|	Add test for NonCumulative inductives	Amin Timany	2017-07-31
\| \| \| \| \| * \| \| \|	Issue error on monomorphic cumulative inductives	Amin Timany	2017-07-31
\| \| \| \| \| \| \|_\|/ \| \| \| \| \| \|/\| \|
* \| \| \| \| / \| \|	closing bug 5315	Julien Forest	2017-07-29
\| \|_\|_\|_\|/ / / \|/\| \| \| \| \| \|
\| \| \| \| * \| \|	Fixing bug #5671 (specialize unclean wrt Metas).	Hugo Herbelin	2017-07-27
\| \|_\|_\|/ / / \|/\| \| \| \| \|
\| \| \| * \| \|	test-suite: more use of the new command Extraction TestCompile	Pierre Letouzey	2017-07-27
* \| \| \| \| \|	Fix TypeclassDebug.out after conflicting PR merges	Matthieu Sozeau	2017-07-26
\| \| \| * \| \|	test-suite/success/extraction.v : add some Extraction TestCompile	Pierre Letouzey	2017-07-26
\| \| \| * \| \|	Enrich test file 4720.v with a compilation test of the extracted code	Pierre Letouzey	2017-07-26
\| \|_\|/ / / \|/\| \| \| \|
\| \| * \| \|	adding a test-suite file 4709.v (thanks to the new command Extraction TestCom...	Pierre Letouzey	2017-07-26
\| \|/ / / \|/\| \| \|
* \| \| \|	Merge PR #918: Extraction: do not mix Haskell types Any and () (fix bugs 4844...	Maxime Dénès	2017-07-26
\|\ \ \ \
\| \| * \| \|	Adding support for recursive notations of the form "x , .. , y , z".	Hugo Herbelin	2017-07-26
\| \|/ / / \|/\| \| \|
* \| \| \|	Merge PR #857: Extraction: various fixes related with bug 4720	Maxime Dénès	2017-07-26
\|\ \ \ \
\| \| * \| \|	Extraction: do not mix Haskell types Any and () (revert 8e257d4, fix bugs 484...	Pierre Letouzey	2017-07-25
\| \|/ / / \|/\| \| \|
\| * \| \|	Extraction: fix bugs 5177 and 5240 (and also indirectly bug 4720)	Pierre Letouzey	2017-07-20
* \| \| \|	fake_ide: do as coqide to find out coqtop path	Enrico Tassi	2017-07-20
* \| \| \|	more verbose logs for coq-makefile	Enrico Tassi	2017-07-20
* \| \| \|	coq-makefile: make test suite detect more errors	Enrico Tassi	2017-07-20
* \| \| \|	Remove trailing CR before diff in output and misc tests.	Maxime Dénès	2017-07-20
* \| \| \|	Print failure logs on appveyor.	Maxime Dénès	2017-07-20
* \| \| \|	Remove non-terminating Timeout tests from Hints.v.	Maxime Dénès	2017-07-20
* \| \| \|	Make coqlib relative in test suite (revert 024a7ab20b0)	Maxime Dénès	2017-07-20
\|/ / /
* \| \|	Merge PR #869: Enforce alternating separators in typeclass debug output	Maxime Dénès	2017-07-20
\|\ \ \
* \ \ \	Merge branch 'v8.7'	Maxime Dénès	2017-07-20
\|\ \ \ \
\| \| \| * \|	Removing testing unsupported Next.	Hugo Herbelin	2017-07-19
\| * \| \| \|	Merge PR #745: Add timing scripts	Maxime Dénès	2017-07-19
\| \|\ \ \ \
\| \| \| \| * \|	Adding a coqdoc target to test-suite.	Hugo Herbelin	2017-07-17
* \| \| \| \| \|	Getting rid of abstraction breaking code in tclABSTRACT.	Pierre-Marie Pédrot	2017-07-14
* \| \| \| \| \|	Removing the uses of abstraction-breaking code in Lemmas.	Pierre-Marie Pédrot	2017-07-13
\| \|_\|_\|/ / \|/\| \| \| \|
* \| \| \| \|	Merge PR #870: Prepare De Bruijn universe abstractions, Episode I: Kernel	Maxime Dénès	2017-07-13
\|\ \ \ \ \
\| \| \| \| * \|	format pairs of items for pr_depth to get alternating separators	Paul Steckler	2017-07-12
\| \|_\|_\|/ / \|/\| \| \| \|
\| \| * \| \|	Deprecate options that were introduced for compatibility with 8.5.	Théo Zimmermann	2017-07-11
\| \|/ / / \|/\| \| \|
\| * \| \|	Fix nonsensical universe abstraction in the kernel.	Pierre-Marie Pédrot	2017-07-11
\| * \| \|	Properly handling polymorphic inductive subtyping in the kernel.	Pierre-Marie Pédrot	2017-07-11
\| * \| \|	Cleaning up the implementation of module subtyping in the kernel.	Pierre-Marie Pédrot	2017-07-11
\| \| * \|	Add timing scripts	Jason Gross	2017-07-11
\| \|/ / \|/\| \|
* \| \|	Merge PR #863: Fixing environment in warning "Projection value has no head co...	Maxime Dénès	2017-07-07
\|\ \ \ \| \|/ / \|/\| \|