coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	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-26
\|
*	More invariants in UState.	Pierre-Marie Pédrot	2015-11-26
\|
*	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
\|
*	Removing some goal unsafeness in inductive schemes.	Pierre-Marie Pédrot	2015-10-29
\|
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-29
\|
*	Removing some unsafe uses of monotonicity.	Pierre-Marie Pédrot	2015-10-19
\|
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-19
\|
*	Adding a notion of monotonous evarmap.	Pierre-Marie Pédrot	2015-10-18
\|
*	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
\|
*	Fix documentation.	Matthieu Sozeau	2015-07-27
\|
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-07-18
\|
*	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-07-02
\|
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-06-28
\|
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-06-01
\|
*	Adding a primitive to the tactic monad to modify the exceptional content.	Pierre-Marie Pédrot	2015-05-07
\|
*	Exposing the minimal amount of internal of the Logic monad in order to	Pierre-Marie Pédrot	2015-05-06
\| \| \| \| \| \| \| \| \|	allow reusability of the implementation throughout the Coq codebase. We effectively feature a generalized version of the logical monad where the input state, the output state and the inner exception can be arbitrarily chosen. This will allow for more efficient implementations of close variants of the monad.
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-05-05
\|
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-03-23
\|
*	Moving Proofview_monad to the engine/ folder.	Pierre-Marie Pédrot	2015-02-28
\|
*	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.