aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/Cases.v
Commit message (Expand)AuthorAge
* Introduce an option to allow nested lemma, and turn it off by default.Gravatar Théo Zimmermann2018-05-17
* In printing, factorizing "match" clauses with same right-hand side.Gravatar Hugo Herbelin2017-12-12
* A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Hugo Herbelin2017-06-09
* Better support for printing constructors with let-ins.Gravatar Hugo Herbelin2017-04-07
* Test for variant of #5142 (good error message on pattern-matching failure).Gravatar Hugo Herbelin2016-10-19
* Attempt to improve error rendering in pattern-matching compilation (#5142).Gravatar Hugo Herbelin2016-10-19
* Fix issues in test-suite revealed by warnings.Gravatar Maxime Dénès2016-06-29
* Using x in output test-suite Cases.v (cosmetic).Gravatar Hugo Herbelin2015-12-05
* Updating test-suite after Bracketing Last Introduction Pattern set byGravatar Hugo Herbelin2015-11-10
* Fixing clash in output test-suite Cases.Gravatar Hugo Herbelin2014-10-23
* A patch for printing "match" when constructors are defined with let-inGravatar Hugo Herbelin2014-10-20
* Fixing #3293 (eta-expansion at "match" printing time was failingGravatar Hugo Herbelin2014-04-28
* Parameters in pattern first step.Gravatar pboutill2012-01-16
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Test case for previous commit.Gravatar msozeau2008-11-27
* Correction de quelques défauts d'affichage (notations sous "as" pourGravatar herbelin2007-10-05
* - Fixing bug 1703 ("intros until n" falls back on the variable name whenGravatar herbelin2007-09-21
* Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8Gravatar herbelin2005-12-21
* Problème de désynchronisation des variables du type et du corps d'un point-...Gravatar herbelin2003-01-15