coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-29
\|
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|
*	Remove useless rec flags.	Guillaume Melquiond	2016-01-02
\|
*	Merge branch 'v8.5' into trunk	Guillaume Melquiond	2015-12-31
\|
*	CLEANUP: in the Reduction module	Matej Kosik	2015-12-17
\|
*	CLEANUP: in the Reduction module	Matej Kosik	2015-12-17
\|
*	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).
*	More efficient implementation of equality-up-to-universes in Universes.	Pierre-Marie Pédrot	2015-11-26
\| \| \| \| \| \|	Instead of accumulating constraints which are not present in the original graph, we parametrize the equality function by a function actually merging those constraints in the current graph. This prevents doing the work twice.
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-20
\|
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-05
\|
*	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.
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-15
\|
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-09
\|
*	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.
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-06
\|
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-02
\|
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-02
\|
*	Removing meta_with_name from Evd.	Pierre-Marie Pédrot	2015-09-27
\|
*	Removing subst_defined_metas_evars from Evd.	Pierre-Marie Pédrot	2015-09-27
\|
*	Removing uselessly duplicated function in Evd.	Pierre-Marie Pédrot	2015-09-27
\|
*	Hardening the API of evarmaps.	Pierre-Marie Pédrot	2015-09-26
\| \| \| \| \| \|	The evar counter has been moved from Evarutil to Evd, and all functions in Evarutil now go through a dedicated primitive to create a fresh evar from an evarmap.
*	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-09-17
\|
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-06-28
\|
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-06-01
\|
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-05-05
\|
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-03-23
\|
*	Adding a new folder corresponding to the low-level part of the pretyper	Pierre-Marie Pédrot	2015-02-27
	together with the tactic monad. The move is not complete yet, because some file candidates for this directory have almost useless dependencies in other ones that should not be moved.