aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/Cases.out
AgeCommit message (Expand)Author
2021-01-13Avoid using "subgoals" in the UI, it means the same as "goals"Jim Fehrle
2021-01-04Temporarily deactivating printing check for cases.Pierre-Marie Pédrot
2020-12-09Fixing support for argument scopes and let-ins while interning cases patterns.Hugo Herbelin
2020-10-05Wish #12762: warning on duplicated catch-all pattern with unused named variable.Hugo Herbelin
2020-08-28In "About", print all arguments, even if it is trailing list of _.Hugo Herbelin
2019-12-03Fixes #11231 (missing dependency in pattern-matching decompilation).Hugo Herbelin
2019-11-20Combine similar arguments when printing Arguments commandGaëtan Gilbert
2019-10-31Fix output testsGaëtan Gilbert
2019-01-09Stop [Print] from saying [is (not) universe polymorphic].Gaëtan Gilbert
2018-12-17Stop printing Monomorphic/Polymorphic in Print.Gaëtan Gilbert
2018-11-02Remove is_universe_polymorphism from printingGaëtan Gilbert
2018-09-27Inference of return clause: giving uniformly priority to "small inversion".Hugo Herbelin
2018-07-25In "redundant clause" pattern-matching error, show also the pattern (#7777).Hugo Herbelin
2017-12-12In printing, factorizing "match" clauses with same right-hand side.Hugo Herbelin
2017-06-09A fix to #5414 (ident bound by ltac names now known for "match").Hugo Herbelin
2017-04-07Better support for printing constructors with let-ins.Hugo Herbelin
2016-10-19Test for variant of #5142 (good error message on pattern-matching failure).Hugo Herbelin
2016-10-19Attempt to improve error rendering in pattern-matching compilation (#5142).Hugo Herbelin
2016-04-04Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Matthieu Sozeau
2015-12-05Using x in output test-suite Cases.v (cosmetic).Hugo Herbelin
2015-11-15Fixing output test Cases.v.Pierre-Marie Pédrot
2015-08-14Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080Jason Gross
2015-03-09Do not display the status of monomorphic constants unless in universe-polymor...Guillaume Melquiond
2014-10-23Fixing clash in output test-suite Cases.Hugo Herbelin
2014-10-20A patch for printing "match" when constructors are defined with let-inHugo Herbelin
2014-08-12Upgrading output tests.Hugo Herbelin
2014-07-21Fixing output test-suite.Pierre-Marie Pédrot
2014-05-08Fixing output test-suite: since universe polymorphism, the Print commandPierre-Marie Pédrot
2014-04-28Fixing #3293 (eta-expansion at "match" printing time was failingHugo Herbelin
2012-05-15Notations are back in the "in" clause of pattern matching.pboutill
2012-01-16Parameters in pattern first step.pboutill
2009-01-02Conséquence renommage canonique de refl_equal en eq_refl.herbelin
2008-11-27Test case for previous commit.msozeau
2008-07-29Update test-suite outputglondu
2007-10-05Correction de quelques défauts d'affichage (notations sous "as" pourherbelin
2007-09-21- Fixing bug 1703 ("intros until n" falls back on the variable name whenherbelin
2006-06-09Adaptation Tactics.out et Cases.out au comportement actuel à défaut d'évit...herbelin
2005-12-21Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8herbelin
2004-12-09MAJ avec les particularités de l'afficheur v7 de la V8herbelin
2003-01-15Problème de désynchronisation des variables du type et du corps d'un point-...herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:39:49 +0000