aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/4198.v
AgeCommit message (Expand)Author
2018-10-04rename test files (do not start by a digit)Vincent Laporte
2018-05-17Introduce an option to allow nested lemma, and turn it off by default.Théo Zimmermann
2016-07-18Fix bug #4923: Warning: appcontext is deprecated.Pierre-Marie Pédrot
2015-05-13Better fixing #4198 such that the term to match is looked for beforeHugo Herbelin
2015-04-22Test for #4198 (appcontext in return clause of match).Hugo Herbelin