coq - The formal proof system

Age	Commit message (Collapse)	Author
2018-10-04	rename test files (do not start by a digit)	Vincent Laporte

2017-08-21	Ensuring all .v files end with a newline to make "sed -i" work better on them.	Hugo Herbelin

2016-10-22	Port fix for bugs 4763, 5149, previously 0b417c12e	Matthieu Sozeau
	Adds a compatibility flag so that the behavior of 8.5 can be obtained too. Original commit: unification.ml: fix for bug #4763, unif regression Do not force all remaining conversions problems to be solved after the _first_ solution of an evar. This was hell to track down, thanks for the help of Maxime. contribs pass and HoTT too.
2016-10-21	Revert "unification.ml: fix for bug #4763, unif regression"	Maxime Dénès
	This reverts commit 0b417c12eb10bb29bcee04384b6c0855cb9de73a. A good fix requires to review a bit the design of unification constraint postponement, which we do in 8.6. We leave things as they are in 8.5 for compatibility.
2016-10-06	unification.ml: fix for bug #4763, unif regression	Matthieu Sozeau
	Do not force all remaining conversions problems to be solved after the _first_ solution of an evar, but only at the end of assignment of terms to evars in w_merge. This was hell to track down, thanks for the help of Maxime. contribs pass and HoTT too.