coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Allow interactive editing of {C,}Morphisms in PG	Jason Gross	2017-04-28
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-30
\|\
\| *	Fix handling of arity of definitional classes.	Matthieu Sozeau	2016-03-24
* \|	Making parentheses mandatory in tactic scopes.	Pierre-Marie Pédrot	2016-03-04
\|/
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Univs: entirely disallow instantiation of polymorphic constants with	Matthieu Sozeau	2015-11-27
*	Univs: add Strict Universe Declaration option (on by default)	Matthieu Sozeau	2015-10-07
*	Universes: enforce Set <= i for all Type occurrences.	Matthieu Sozeau	2015-10-02
*	Fix instances of universe-polymorphic generalized rewriting to avoid	Matthieu Sozeau	2015-04-09
*	Update headers.	Maxime Dénès	2015-01-12
*	Move to a representation of universe polymorphic constants using indices for ...	Matthieu Sozeau	2014-08-03
*	Export the right modules in Setoid, avoiding anomalies in generalized rewriting.	Matthieu Sozeau	2014-06-26
*	- Fix in kernel conversion not folding the universe constraints	Matthieu Sozeau	2014-05-26
*	Update and start testing rewrite-in-type code.	Matthieu Sozeau	2014-05-09
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06