coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possible	Matthieu Sozeau	2014-08-25
*	CPS-style tactic matching. We use the tactic monad as the target of the CPS.	Pierre-Marie Pédrot	2014-07-28
*	Small code sharing in TacticMatching.	Pierre-Marie Pédrot	2014-07-22
*	Using IStream coiterator to explicit the captured state of tactic matching re...	Pierre-Marie Pédrot	2014-07-05
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Remove some dead-code (thanks to ocaml warnings)	Pierre Letouzey	2014-03-05
*	Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)	Pierre Letouzey	2014-03-02
*	TacticMatching: avoid some closure allocation in (<*>).	Arnaud Spiwack	2014-02-24
*	Removed some trailing whitespaces.	Arnaud Spiwack	2014-02-24
*	IStream: a concat_map primitive.	Arnaud Spiwack	2014-02-24
*	Optimization: in case of empty substitution, merging is trivial.	Pierre-Marie Pédrot	2013-11-19
*	Slightly faster version of merging substitutions in TacticMatching.	ppedrot	2013-11-16
*	Implementation of Ltac's match and match goal fully based on IStream.	aspiwack	2013-11-14