aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure/proofirrelevance.v
Commit message (Collapse)AuthorAge
* Update various comments to use "template polymorphism"Gravatar Gaetan Gilbert2017-04-11
| | | | Also remove obvious comments.
* Use "Fail" rather than rely on exit code.Gravatar xclerc2013-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16792 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* Check that sort-polymorphic inductive types is not too laxGravatar herbelin2006-10-27
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9297 85f007b7-540e-0410-9357-904b9bb8a0f7