coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	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
\| \| \| \| * \| \| \| \| \| \| \| \|	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
\| \| \| \| * \| \| \| \| \| \| \| \|	Extend definition of inductives to include subtyping info	Amin Timany	2017-06-16
\| \|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \|	Move TIMER to right in front of COQC	Jason Gross	2017-06-15
\| \| \| \| \| \| \| \| \| \| * \|	Fix `make TIMED=1` garbage	Jason Gross	2017-06-15
\| \| \| \| \| \| \| \| \| \| * \|	Strip trailing whitespace	Jason Gross	2017-06-15
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \|	Merge PR#748: [stm] More fixes for nested commands [bugzilla 5589]	Maxime Dénès	2017-06-15
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR#778: Revert "[travis] temporary UniMath overlay"	Maxime Dénès	2017-06-15
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#719: Constrexpr.Numeral without bigint	Maxime Dénès	2017-06-15
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#769: [lib] Remove obsolete state-management function add_frozen_state	Maxime Dénès	2017-06-15
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \| \| \| \| \| \| \| \| \| \| \| \| \| \|	fix dev/base_include (thanks Zimmi48)	Pierre Letouzey	2017-06-15
* \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Makefile.build : restore (temporarily?) the anti-cmi-corruption hacks	Pierre Letouzey	2017-06-15