coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
\|\ \ \
* \ \ \	Merge PR#787: [typeclasses eauto] Fix bug #3943: non-termination in topological	Maxime Dénès	2017-06-19
\|\ \ \ \
* \ \ \ \	Merge PR#760: Fixing base_include after loc is an option + a better test that...	Maxime Dénès	2017-06-19
\|\ \ \ \ \
* \ \ \ \ \	Merge PR#613: Cumulativity for inductive types	Maxime Dénès	2017-06-19
\|\ \ \ \ \ \
* \| \| \| \| \| \|	Test case for bug 5578.	Maxime Dénès	2017-06-19
\| \| \| \| * \| \|	romega: avoid potential slowdown when changing concl by reified version	Pierre Letouzey	2017-06-16
* \| \| \| \| \| \|	Increase the time limit on 4366.v to make gitlab work better.	Gaëtan Gilbert	2017-06-16
\| \|_\|_\|/ / / \|/\| \| \| \| \|
\| * \| \| \| \|	Fix a bug in cumulativity	Amin Timany	2017-06-16
\| * \| \| \| \|	Clean up universes of constants and inductives	Amin Timany	2017-06-16
\| * \| \| \| \|	Move (part of) tests from checker to success	Amin Timany	2017-06-16
\| * \| \| \| \|	Checker add test for non-trivial constraints	Amin Timany	2017-06-16
\| * \| \| \| \|	Change the option to Set Inductive Cumulativity	Amin Timany	2017-06-16
\| * \| \| \| \|	Correct coqchk reduction	Amin Timany	2017-06-16
\| * \| \| \| \|	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
\| \| \| \| \|\