coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Print [Variant] types with the keyword [Variant].	Arnaud Spiwack	2014-09-04
*	Fixing universe substitution in mutual fixpoints.	Pierre-Marie Pédrot	2014-07-16
*	Better handling of the universe context in case of Admitted proof obligations.	Matthieu Sozeau	2014-07-10
*	all coqide specific files moved into ide/	Enrico Tassi	2014-06-25
*	Fix handling of side effects in Defined objects (Closes: HoTT#111 + 3344)	Enrico Tassi	2014-06-23
*	Proofs now take and return an evar_universe_context, simplifying interfaces	Matthieu Sozeau	2014-06-18
*	Moving hook code from Future to Lemmas. This seemed to disrupt compilation of	Pierre-Marie Pédrot	2014-06-08
*	Enforce a correct exception handling in declaration_hooks	Enrico Tassi	2014-06-08
*	- Fix in kernel conversion not folding the universe constraints	Matthieu Sozeau	2014-05-26
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06
*	Adapt universe polymorphic branch to new handling of futures for delayed proofs.	Matthieu Sozeau	2014-05-06
*	Lemmas: export standard proof terminator	Enrico Tassi	2014-05-06
*	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau	2014-05-06
*	Rework handling of universes on top of the STM, allowing for delayed	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Adding a stm/ folder, as asked during last workgroup. It was essentially moving	Pierre-Marie Pédrot	2014-04-25