coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
\|\ \ \ \
* \| \| \| \|	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
\|\ \
\| * \	Merge PR #745: Add timing scripts	Maxime Dénès	2017-07-19
\| \|\ \
* \| \| \|	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
\|\ \ \
* \ \ \	Merge PR#826: Put plugin exports in the right compatibility file	Maxime Dénès	2017-06-26
\|\ \ \ \
* \ \ \ \	Merge PR#828: closing bug #4250	Maxime Dénès	2017-06-26
\|\ \ \ \ \ \| \| \|_\|/ / \| \|/\| \| \|
* \| \| \| \|	Merge PR#794: Cleanup of ltac cmxs	Maxime Dénès	2017-06-23
\|\ \ \ \ \
\| \| * \| \| \|	closing bug #4250	Julien Forest	2017-06-23
\| \|/ / / / \|/\| \| \| \|
\| \| \| \| *	Add tests for handling of warnings	Tej Chajed	2017-06-23
\| \| * \| \|	Add test-suite file for funind, extraction with compat 8.6	Jason Gross	2017-06-22
\| \|/ / / \|/\| \| \|
\| \| * \|	Should fix a false negative reported by deps-order.sh.	Hugo Herbelin	2017-06-21
\| \|/ / \|/\| \|
* \| \|	Merge PR#807: romega: fix a slowdown	Maxime Dénès	2017-06-20
\|\ \ \