coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Define and use UGraph.enforce_leq_alg for subtyping inference	Gaëtan Gilbert	2018-06-22
\| \| \| \|	Not sure if worth using in other places.
*	Fix restrict_universe_context	Gaëtan Gilbert	2018-05-30
\|
*	universe normalisation: put equivalence class partition in UGraph	Gaëtan Gilbert	2018-04-13
\| \| \| \|	ie don't go through having Eq constraints but directly to the unionfind.
*	Replace invalid tag @raises in ocamldoc comments with @raise	mrmr1993	2018-03-05
\|
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|
*	[api] Remove yet another type alias.	Emilio Jesus Gallego Arias	2017-12-09
\|
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
\| \| \| \|	We do up to `Term` which is the main bulk of the changes.
*	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.