coq - The formal proof system

Age	Commit message (Collapse)	Author
2017-02-14	Namegen primitives now apply on evar constrs.	Pierre-Marie Pédrot
	Incidentally, this fixes a printing bug in output/inference.v where the displayed name of an evar was the wrong one because its type was not evar-expanded enough.
2016-11-08	Introducing a new EConstr.t type to perform the nf_evar operation on demand.	Pierre-Marie Pédrot

2016-10-30	Moving Universes to the engine/ folder.	Pierre-Marie Pédrot
	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.
2016-10-30	Reordering Termops w.r.t. Evd and Namegen in engine folder.	Pierre-Marie Pédrot

2016-05-04	Moving Ftactic and Geninterp to the engine folder.	Pierre-Marie Pédrot

2016-03-20	Moving Evarutil and Proofview to engine/	Pierre-Marie Pédrot

2015-10-18	Adding a notion of monotonous evarmap.	Pierre-Marie Pédrot

2015-10-17	Dedicated file for universe unification context manipulation.	Pierre-Marie Pédrot
	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.
2015-02-28	Moving Proofview_monad to the engine/ folder.	Pierre-Marie Pédrot

2015-02-27	Adding a new folder corresponding to the low-level part of the pretyper	Pierre-Marie Pédrot
	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.