aboutsummaryrefslogtreecommitdiff
path: root/test-suite/failure/inductive3.v
AgeCommit message (Collapse)Author
2013-09-20Merge "inductive?.v" tests into a single "inductive.v" test.xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16798 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-20Use "Fail" rather than rely on exit code.xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16792 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-23Stricte positivité en présence de types inductifs imbriqués avec ↵herbelin
paramètres récursivement non uniformes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8987 85f007b7-540e-0410-9357-904b9bb8a0f7