coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Adding mention of shelved/given-up status in "Show Existentials".	Hugo Herbelin	2018-02-22
\| \| \| \| \| \|	Also changed the API of pr_subgoals now using labels. Also removed a trailing space in printing existentials.
*	Do not give a name to anonymous evars anymore. See bug #4547.	Pierre-Marie Pédrot	2016-02-13
\| \| \| \| \| \| \| \|	The current solution may not be totally ideal though. We generate names for anonymous evars on the fly at printing time, based on the Evar_kind data they are wearing. This means in particular that the printed name of an anonymous evar may change in the future because some unrelate evar has been solved or introduced.
*	Fixing output test Existentials.v after eec77191b.	Hugo Herbelin	2015-11-07
\|
*	Adapting output tests to current naming of evars, even if unclear	Hugo Herbelin	2014-11-11
\| \| \| \|	where it will eventually stabilize.
*	An evar name changed in output test.	Hugo Herbelin	2014-10-02
\|
*	Adapting to naming of evars.	Hugo Herbelin	2014-09-27
\|
*	Test suite: update output reference.	xclerc	2013-12-02
\|
*	Fixing 2 output test-suites.	ppedrot	2013-10-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16863 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Adapting test Existentials to new numbering strategy of evars (r14764).	herbelin	2011-12-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14777 85f007b7-540e-0410-9357-904b9bb8a0f7
*	test-suite: fix output/Existentials.out	glondu	2010-10-06
\| \| \| \| \| \| \|	The new output makes sense with the new "1 subgoal = 1 evar" paradigm introduced with by the new proof engine. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13508 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix test output mentionning an existential number that changed.	msozeau	2009-04-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12096 85f007b7-540e-0410-9357-904b9bb8a0f7
*	The initial state evar numbering increased. Fix output message in a test.	puech	2009-01-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11805 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Regression test for bug #1967	herbelin	2009-01-02
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11740 85f007b7-540e-0410-9357-904b9bb8a0f7