coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR#787: [typeclasses eauto] Fix bug #3943: non-termination in topological	Maxime Dénès	2017-06-19
\|\
* \	Merge PR#777: Improving documentation of tactic "move" (report #4561)	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#795: [ide] Better exn printing. [fixes BZ#5524]	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
* \| \| \| \| \|	Merge PR#727: [tactics] Fix summary registration of global hint variable.	Maxime Dénès	2017-06-19
\|\ \ \ \ \ \
* \| \| \| \| \| \|	Fix typo in comment.	Maxime Dénès	2017-06-19
* \| \| \| \| \| \|	Merge PR#784: API additions for coq-dpdgraph	Maxime Dénès	2017-06-19
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR#755: "There are pending proofs" error message now lists the name of ...	Maxime Dénès	2017-06-19
\|\ \ \ \ \ \ \ \
\| \| \| \| \| * \| \| \|	[ide] Better exn printing. [fixes BZ#5524]	Emilio Jesus Gallego Arias	2017-06-18
* \| \| \| \| \| \| \| \|	Merge PR#804: Increase the time limit on 4366.v to make gitlab work better.	Maxime Dénès	2017-06-16
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR#759: don't leak unqualified identifiers from the macro	Maxime Dénès	2017-06-16
\|\ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \|	Add coq-dpdgraph to gitlab CI	Gaëtan Gilbert	2017-06-16
\| \| \| * \| \| \| \| \| \|	"There are pending proofs" error message now lists the name of the proofs.	Théo Zimmermann	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
\| \| \| \| * \| \| \|	A short cleanup	Amin Timany	2017-06-16
\| \| \| \| * \| \| \|	use map_constr more efficiently	Amin Timany	2017-06-16
\| \| \| \| * \| \| \|	Optimization	Amin Timany	2017-06-16
\| \| \| \| * \| \| \|	Use a smart map_constr	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
\| \| \| \| * \| \| \|	Remove Warnings: unused value ...	Amin Timany	2017-06-16
\| \| \| \| * \| \| \|	Checker add test for non-trivial constraints	Amin Timany	2017-06-16
\| \| \| \| * \| \| \|	Properly instantiate contexts before pushing	Amin Timany	2017-06-16
\| \| \| \| * \| \| \|	Enable the checking of ind subtyping in checker	Amin Timany	2017-06-16
\| \| \| \| * \| \| \|	Document cumulativity for inductive types	Amin Timany	2017-06-16
\| \| \| \| * \| \| \|	Change the option to Set Inductive Cumulativity	Amin Timany	2017-06-16
\| \| \| \| * \| \| \|	Add printing of cumulativity in inductive types	Amin Timany	2017-06-16
\| \| \| \| * \| \| \|	Move univops from kernel to library	Amin Timany	2017-06-16
\| \| \| \| * \| \| \|	Correct coqchk checking subtyping relation for inductives	Amin Timany	2017-06-16
\| \| \| \| * \| \| \|	Correct coqchk reduction	Amin Timany	2017-06-16
\| \| \| \| * \| \| \|	Simplify Univ.ml	Amin Timany	2017-06-16
\| \| \| \| * \| \| \|	Fix a bug	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
\| \| \| \| * \| \| \|	Squashed commit of the following:	Amin Timany	2017-06-16
\| \| \| \| * \| \| \|	Make unification use subtyping info of inductives	Amin Timany	2017-06-16
\| \| \| \| * \| \| \|	Fix cum/conv for inductive types	Amin Timany	2017-06-16
\| \| \| \| * \| \| \|	Use inductive subtyping for conv/cumul	Amin Timany	2017-06-16
\| \| \| \| * \| \| \|	Change the place of inference after sect discharge	Amin Timany	2017-06-16
\| \| \| \| * \| \| \|	Subtyping inference for inductoves and records	Amin Timany	2017-06-16
\| \| \| \| * \| \| \|	Add subtyping inference for inductive types	Amin Timany	2017-06-16
\| \| \| \| * \| \| \|	Correct subtyping check for constructors	Amin Timany	2017-06-16
\| \| \| \| * \| \| \|	Fix typo in error message	Amin Timany	2017-06-16
\| \| \| \| * \| \| \|	Check subtyping of inductive types in Kernel	Amin Timany	2017-06-16
\| \| \| \| * \| \| \|	Using UInfoInd for universes in inductive types	Amin Timany	2017-06-16
\| \| \| \| * \| \| \|	New datastructure for universes of inductive types	Amin Timany	2017-06-16