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
\|
*	Ensuring all .v files end with a newline to make "sed -i" work better on them.	Hugo Herbelin	2017-08-21
\|
*	congruence fix: test-suite code and update CHANGES	Matthieu Sozeau	2016-07-05
\| \| \| \|	This fixes bugs #4069 (not 4609 as mentionned in the git log) and #4718.
*	congruence/univs: properly refresh (fix #4609)	Matthieu Sozeau	2016-07-04
\| \| \| \| \| \| \|	In congruence, refresh universes including the Set/Prop ones so that congruence works with cumulativity, not restricting itself to the inferred types of terms that are manipulated but allowing them to be used at more general types. This fixes bug #4609.
*	Fix bug #4069: f_equal regression.	Matthieu Sozeau	2015-10-07