aboutsummaryrefslogtreecommitdiff
path: root/test-suite/modules/injection_discriminate_inversion.v
AgeCommit message (Collapse)Author
2017-08-21Ensuring all .v files end with a newline to make "sed -i" work better on them.Hugo Herbelin
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-12-22remplacement d'un test d'egalite par un test de convertibilite dans ↵jforest
injection/discriminate/inversion pour corriger des bugs en presence de modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9459 85f007b7-540e-0410-9357-904b9bb8a0f7