coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Adding a bit of documentation in the mli.	Pierre-Marie Pédrot	2016-06-09
\|
*	Allowing to attach location to universes in UState.	Pierre-Marie Pédrot	2016-02-19
\|
*	Fixing compilation of mli documentation.	Hugo Herbelin	2015-12-05
\| \| \| \| \|	Using dummy comment to @raise to please ocamldoc. Please change MS or PMP, if needed.
*	Remove unneeded fixpoint in normalize_context_set. Note that it is no	Matthieu Sozeau	2015-12-01
\| \| \| \| \| \|	longer stable w.r.t. equality constraints as the universe graph will choose different canonical levels depending on the equalities given to it (l = r vs r = l).
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-30
\|
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-29
\|
*	Clarifying and documenting the UState API.	Pierre-Marie Pédrot	2015-10-17
\|
*	Dedicated file for universe unification context manipulation.	Pierre-Marie Pédrot	2015-10-17
	This allows to remove a lot of independent code from Evd which was put into the UState module. The API is not perfect yet, but this is a first pass. Names of data structures should be thought about too because they are way too similar.