coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Port fix for bugs 4763, 5149, previously 0b417c12e	Matthieu Sozeau	2016-10-22
\| \| \| \| \| \| \| \| \| \| \|	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.
*	Add regression tests for univ. poly. and prim proj	Jason Gross	2014-05-06
	These regression tests are aggregated from the various bugs I (and others) have reported on https://github.com/HoTT/coq/issues relating to universe polymorphism, primitive projections, and eta for records. These are the tests that trunk currently passes. I'm not sure about the naming scheme (HoTT_coq_###.v, where ### is the number of the issue in GitHub), but I couldn't think of a better one.