coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
\|\ \
* \ \	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
\|\ \ \| \|/ \|/\|
\| *	Fixing environment in warning "Projection value has no head constant".	Hugo Herbelin	2017-07-07
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-07-04
\|\ \
* \| \|	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\| \|/ \|/\|
* \|	Merge PR#843: closing bug #5618 introduce by PR 828	Maxime Dénès	2017-06-30
\|\ \
\| * \|	closing bug #5618 introduce by PR 828	Julien Forest	2017-06-29
* \| \|	Merge PR#810: An attempt to fix a failure of test deps-checksum.sh fails with...	Maxime Dénès	2017-06-27
\|\ \ \