coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Make the Constr.kind_of_term type parametric in sorts and universes.	Pierre-Marie Pédrot	2017-03-31
\|
*	Evarconv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Stronger static invariant in equality upto universes.	Pierre-Marie Pédrot	2016-10-31
\| \| \| \| \|	We return an option type, as constraints were always dropped if the boolean was false. They did not make much sense anyway.
*	Moving Universes to the engine/ folder.	Pierre-Marie Pédrot	2016-10-30
	Before this patch, this module was a member of the library folder, which had little to do with its actual use. A tiny part relative to global registering of universe names has been effectively moved to the Global module.