aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/Existentials.out
AgeCommit message (Collapse)Author
2018-02-22Adding mention of shelved/given-up status in "Show Existentials".Hugo Herbelin
Also changed the API of pr_subgoals now using labels. Also removed a trailing space in printing existentials.
2016-02-13Do not give a name to anonymous evars anymore. See bug #4547.Pierre-Marie Pédrot
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.
2015-11-07Fixing output test Existentials.v after eec77191b.Hugo Herbelin
2014-11-11Adapting output tests to current naming of evars, even if unclearHugo Herbelin
where it will eventually stabilize.
2014-10-02An evar name changed in output test.Hugo Herbelin
2014-09-27Adapting to naming of evars.Hugo Herbelin
2013-12-02Test suite: update output reference.xclerc
2013-10-08Fixing 2 output test-suites.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16863 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-07Adapting test Existentials to new numbering strategy of evars (r14764).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14777 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-06test-suite: fix output/Existentials.outglondu
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
2009-04-20Fix test output mentionning an existential number that changed.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12096 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-19The initial state evar numbering increased. Fix output message in a test.puech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11805 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-02Regression test for bug #1967herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11740 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 04:47:12 +0000