coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
\|/
*	Making the strategy type in Rewrite opaque.	Pierre-Marie Pédrot	2015-05-05
*	Update headers.	Maxime Dénès	2015-01-12
*	Attempt to organize and document unification flags of setoid rewrite.	Hugo Herbelin	2014-11-22
*	Removing dead code in Rewrite.	Pierre-Marie Pédrot	2014-10-21
*	Rewrite.apply_strategy uses the same return type as strategies.	Pierre-Marie Pédrot	2014-09-14
*	Proper type for rewrite strategy results.	Pierre-Marie Pédrot	2014-09-14
*	Use an AST for strategy names.	Matthieu Sozeau	2014-09-11
*	Redo PMP's patch to rewriting to make it purely functional using state passing.	Matthieu Sozeau	2014-07-14
*	Fix bug #3291, stack overflow in rewrite.	Matthieu Sozeau	2014-06-11
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Removing unused tactics in rewrite.	Pierre-Marie Pédrot	2014-01-14
*	The tactic [admit] exits with the "unsafe" status.	aspiwack	2013-11-02
*	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack	2013-11-02
*	Opacifying the type of strategies.	ppedrot	2013-09-26
*	Splitting Rewrite into a code part and a CAMLP4-dependent one.	ppedrot	2013-09-26