aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/MatchFail.v
Commit message (Expand)AuthorAge
* Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8Gravatar herbelin2005-12-21
* I added a comment on the tactic compute_POS.Gravatar bertot2002-06-07
* This example does not work in coq-7.3, but does in coq-7.2.Gravatar bertot2002-06-07