aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/MatchFail.v
AgeCommit message (Expand)Author
2005-12-21Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8herbelin
2002-06-07I added a comment on the tactic compute_POS.bertot
2002-06-07This example does not work in coq-7.3, but does in coq-7.2.bertot