coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Introduce an option to allow nested lemma, and turn it off by default.	Théo Zimmermann	2018-05-17
\|
*	Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possible	Matthieu Sozeau	2014-08-25
	to match on a primitive projection application c.(p) using "?f _", binding f to (fun x => x.(p)) with the correct typing.