coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[flags] Remove XML output flag.	Emilio Jesus Gallego Arias	2017-08-01
\| \| \| \| \| \| \| \|	This is a second try at removing the hooks for the legacy xml export system which can't currently be tested. It is also not included in the API, so it should either be included in it or this PR be applied.
*	remove unneeded -emacs flag to coq-prog-args	Paul Steckler	2017-05-01
\|
*	- Fix xml plugin treatment of inductives.	Matthieu Sozeau	2014-06-15
\| \| \| \|	- Move HoTT bug #30 to closed
*	Move opened bugs to bugs/opened	Jason Gross	2014-05-10
\|
*	Add more regression tests for univ poly/prim proj	Jason Gross	2014-05-10
	hese 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 fails. 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.