coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fix UGraph.check_eq!	Matthieu Sozeau	2016-11-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Universes are kept in normal form w.r.t. equality but not the <= relation, so the previous check worked almost always but was actually too strict! In cases like (max(Set,u) = u) when u is declared >= Set it was failing to find an equality. Applying the KISS principle: u = v <-> u <= v /\ v <= u. Fix invariant breakage that triggered the discovery of the check_eq bug as well. No algebraic universes should appear in a term position (on the left of a colon in a typing judgment), this was not the case when an algebraic universe instantiated an evar that appeared in the term. We force their universe variable status to change in refresh_universes to avoid this. Fix ind sort inference: Use syntactic universe equality for inductive sort inference instead of check_leq (which now correctly takes constraints into account) and simplify code
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵	Pierre Letouzey	2016-07-03
\| \| \| \| \| \|	module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
*	Universes algorithm : clarified comments	Jacques-Henri Jourdan	2016-01-17
\|
*	Fix typos.	Guillaume Melquiond	2016-01-01
\|
*	Removing dead code.	Pierre-Marie Pédrot	2015-12-27
\|
*	New algorithm for universe cycle detections.	Jacques-Henri Jourdan	2015-12-01
\|
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-26
\|
*	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.