aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/CaseInClause.v
AgeCommit message (Collapse)Author
2018-10-04test-suite: cleaningVincent Laporte
2016-10-17Example illustrating non-local inference of the default type of impossible ↵Hugo Herbelin
branches (see PR #323).
2016-04-27Fixing a "This clause is redundant" error when interpreting the "in"Hugo Herbelin
clause of a "match" over an irrefutable pattern.
2013-01-21Fix bug 2958: Inductive deep in in clause are impossiblepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16133 85f007b7-540e-0410-9357-904b9bb8a0f7