coq - The formal proof system

Age	Commit message (Collapse)	Author
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.