coq - The formal proof system

Age	Commit message (Collapse)	Author
2016-11-30	Fix UGraph.check_eq!	Matthieu Sozeau
	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
2016-07-03	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵	Pierre Letouzey
	module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
2016-01-17	Universes algorithm : clarified comments	Jacques-Henri Jourdan

2016-01-01	Fix typos.	Guillaume Melquiond

2015-12-27	Removing dead code.	Pierre-Marie Pédrot

2015-12-01	New algorithm for universe cycle detections.	Jacques-Henri Jourdan

2015-11-26	Merge branch 'v8.5'	Pierre-Marie Pédrot

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.