coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-27
\|
*	Cleaning up the implementation of module subtyping in the kernel.	Pierre-Marie Pédrot	2017-07-11
\| \| \| \| \| \| \| \|	We export a function in UGraph to check that a polymorphic instance is a subtype of another, instead of rolling up our own in module code. We also add a few tests for module subtyping in presence of polymorphic constants.
*	Merge PR#518: Faster universe unification	Maxime Dénès	2017-05-23
\|\
* \|	Remove some unused values and types	Gaetan Gilbert	2017-04-27
\| \|
\| *	Fast path when checking equality of universe levels in UState.	Pierre-Marie Pédrot	2017-04-27
\|/ \| \| \| \|	We export the relevant level equality function in UGraph which is way faster than checking that each one is smaller than the other as universes.
*	Splitting kernel universe code in two modules.	Pierre-Marie Pédrot	2015-10-06
	1. The Univ module now only cares about definitions about universes. 2. The UGraph module contains the algorithm responsible for aciclicity.