coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 (clause...	Maxime Dénès	2017-11-20
\|\
\| *	One more step in fixing #5762 ("where" clause).	Hugo Herbelin	2017-11-14
* \|	Merge PR #922: New beta-iota compatibility refinements	Maxime Dénès	2017-11-08
\|\ \ \| \|/ \|/\|
* \|	Merge PR #1139: Add a linter.	Maxime Dénès	2017-11-06
\|\ \
\| * \|	Put newlines at the end of files.	Gaëtan Gilbert	2017-10-25
* \| \|	Moving bug numbers to BZ# format in the test-suite.	Théo Zimmermann	2017-10-19
* \| \|	Merge PR #768: Omega and romega know about context definitions (fix old bug 148)	Maxime Dénès	2017-10-10
\|\ \ \
* \| \| \|	[ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.	Emilio Jesus Gallego Arias	2017-10-05
\| \|/ / \|/\| \|
\| * \|	romega: takes advantage of context variables with body	Pierre Letouzey	2017-10-05
\|/ /
* \|	Merge PR #1101: Fixing an old proof engine bug in collecting evars with clear...	Maxime Dénès	2017-10-05
\|\ \
* \| \|	[vernac] Remove `Qed exporting` syntax.	Emilio Jesus Gallego Arias	2017-09-29
\| * \|	Fixing an old bug in collecting evars with cleared context.	Hugo Herbelin	2017-09-27
\|/ /
* \|	Merge PR #688: Binding universe constraints in Definition/Inductive/etc...	Maxime Dénès	2017-09-26
\|\ \
* \| \|	Fixing _rect bug for inductive types with let-ins and non-rec uniform params.	Hugo Herbelin	2017-09-23
\| * \|	test-suite: polymorphism	Matthieu Sozeau	2017-09-19
\| * \|	Allow declaring universe binders with no constraints with @{\|}	Gaëtan Gilbert	2017-09-19
\| * \|	Allow declaring universe constraints at definition level.	Matthieu Sozeau	2017-09-19
* \| \|	Merge PR #920: kernel: bugfix in filter_stack_domain.	Maxime Dénès	2017-09-19
\|\ \ \ \| \|/ / \|/\| \|
\| * \|	Add test-suite script by Cyprien Mangin	Matthieu Sozeau	2017-09-18
* \| \|	Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" work...	Maxime Dénès	2017-09-15
\|\ \ \
* \| \| \|	Fixing little inaccuracy in coercions to ident or name.	Hugo Herbelin	2017-09-12
* \| \| \|	Merge PR #830: Moving assert (the "Cut" rule) to new proof engine	Maxime Dénès	2017-08-29
\|\ \ \ \
\| \| * \| \|	Ensuring all .v files end with a newline to make "sed -i" work better on them.	Hugo Herbelin	2017-08-21
\| \|/ / / \|/\| \| \|
\| \| \| *	Fixing another regression with 8.4 wrt to βι-normalization of created hyps.	Hugo Herbelin	2017-08-21
\| \| \| *	Fixing a new regresssion with 8.4 wrt to βι-normalization of created hyps.	Hugo Herbelin	2017-08-21
\| \|_\|/ \|/\| \|
* \| \|	Merge PR #864: Some cleanups after cumulativity for inductive types	Maxime Dénès	2017-08-16
\|\ \ \
\| * \| \|	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
\| \| \|/ \| \|/\|
* \| \|	test-suite: more use of the new command Extraction TestCompile	Pierre Letouzey	2017-07-27
* \| \|	test-suite/success/extraction.v : add some Extraction TestCompile	Pierre Letouzey	2017-07-26
\|/ /
* \|	Remove non-terminating Timeout tests from Hints.v.	Maxime Dénès	2017-07-20
* \|	Getting rid of abstraction breaking code in tclABSTRACT.	Pierre-Marie Pédrot	2017-07-14
* \|	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\| *	Reorganizing functions to find the relative position of an hypothesis.	Hugo Herbelin	2017-06-25
\| *	Moving "assert" (internally "Cut") to the new proof engine.	Hugo Herbelin	2017-06-25
* \|	Add test-suite file for funind, extraction with compat 8.6	Jason Gross	2017-06-22
\|/
*	Merge PR#807: romega: fix a slowdown	Maxime Dénès	2017-06-20
\|\
\| *	romega: avoid potential slowdown when changing concl by reified version	Pierre Letouzey	2017-06-16
* \|	Fix a bug in cumulativity	Amin Timany	2017-06-16
* \|	Move (part of) tests from checker to success	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#375: Deprecation	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
\| \| *	Remove support for Coq 8.4.	Guillaume Melquiond	2017-06-14
\| \|/ \|/\|
* \|	Merge PR#498: Bignums as a separate opam package	Maxime Dénès	2017-06-14
\|\ \