coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-01
\|\
\| *	Pfedit.get_current_context refinement (fix #4523)	Matthieu Sozeau	2016-05-26
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Reduce dependencies of interface files.	Guillaume Melquiond	2016-01-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-29
\|\\|
\| *	Univs: correctly register universe binders for lemmas.	Matthieu Sozeau	2015-11-28
* \|	More potentialities in proof_terminators.	Pierre-Marie Pédrot	2015-09-08
\|/
*	Documentation by giving a name to a large type.	Pierre-Marie Pédrot	2015-08-19
*	Removing dead code.	Pierre-Marie Pédrot	2015-02-02
*	Update headers.	Maxime Dénès	2015-01-12
*	Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.	Arnaud Spiwack	2014-10-22
*	Better handling of the universe context in case of Admitted proof obligations.	Matthieu Sozeau	2014-07-10
*	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
*	- Fix in kernel conversion not folding the universe constraints	Matthieu Sozeau	2014-05-26
*	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