coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Moving Ftactic and Geninterp to the engine folder.	Pierre-Marie Pédrot	2016-05-04
\|
*	Moving Evarutil and Proofview to engine/	Pierre-Marie Pédrot	2016-03-20
\|
*	Adding a notion of monotonous evarmap.	Pierre-Marie Pédrot	2015-10-18
\|
*	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.
*	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.