coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Introducing a new EConstr.t type to perform the nf_evar operation on demand.	Pierre-Marie Pédrot	2016-11-08
\|
*	Moving Universes to the engine/ folder.	Pierre-Marie Pédrot	2016-10-30
\| \| \| \| \| \|	Before this patch, this module was a member of the library folder, which had little to do with its actual use. A tiny part relative to global registering of universe names has been effectively moved to the Global module.
*	Reordering Termops w.r.t. Evd and Namegen in engine folder.	Pierre-Marie Pédrot	2016-10-30
\|
*	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.