coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Remove dead code [Universes.simplify_universe_context]	Gaëtan Gilbert	2017-06-20
*	Merge PR#742: Fix `make TIMED=1` garbage	Maxime Dénès	2017-06-20
\|\
* \	Merge PR#774: [ide] Add route_id parameter to query call.	Maxime Dénès	2017-06-20
\|\ \
* \ \	Merge PR#793: Fixing restriction of existential variables regarding evar_store	Maxime Dénès	2017-06-20
\|\ \ \
* \ \ \	Merge PR#807: romega: fix a slowdown	Maxime Dénès	2017-06-20
\|\ \ \ \
* \ \ \ \	Merge PR#803: Clean ssr	Maxime Dénès	2017-06-20
\|\ \ \ \ \
* \ \ \ \ \	Merge PR#790: Direct link to Travis branch builds.	Maxime Dénès	2017-06-20
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR#779: Each user overlay goes into its own file.	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#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] Add route_id parameter to query call.	Emilio Jesus Gallego Arias	2017-06-18
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \|	[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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	romega: avoid potential slowdown when changing concl by reified version	Pierre Letouzey	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
\| \|/ / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \| \| \| \|	Each user overlay goes into its own file.	Théo Zimmermann	2017-06-16
\| \| \| \| \| \| \| \| \| \| * \| \|	Removing Proof_type from the API.	Pierre-Marie Pédrot	2017-06-16
\| \| \| \| \| \| \| \| \| \| * \| \|	Remove the last use of the low-level Proof_type API in ssr.	Pierre-Marie Pédrot	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