coq - The formal proof system

Age	Commit message (Collapse)	Author
2018-06-22	Define and use UGraph.enforce_leq_alg for subtyping inference	Gaëtan Gilbert
	Not sure if worth using in other places.
2018-05-30	Fix restrict_universe_context	Gaëtan Gilbert

2018-04-13	universe normalisation: put equivalence class partition in UGraph	Gaëtan Gilbert
	ie don't go through having Eq constraints but directly to the unionfind.
2018-03-05	Replace invalid tag @raises in ocamldoc comments with @raise	mrmr1993

2018-02-27	Update headers following #6543.	Théo Zimmermann

2017-12-09	[api] Remove yet another type alias.	Emilio Jesus Gallego Arias

2017-11-06	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias
	We do up to `Term` which is the main bulk of the changes.
2017-07-27	deprecate Pp.std_ppcmds type alias	Matej Košík

2017-07-11	Cleaning up the implementation of module subtyping in the kernel.	Pierre-Marie Pédrot
	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.
2017-05-23	Merge PR#518: Faster universe unification	Maxime Dénès

2017-04-27	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
	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.
2015-10-06	Splitting kernel universe code in two modules.	Pierre-Marie Pédrot
	1. The Univ module now only cares about definitions about universes. 2. The UGraph module contains the algorithm responsible for aciclicity.