aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/MatchFail.v
AgeCommit message (Expand)Author
2016-03-04Making parentheses mandatory in tactic scopes.Pierre-Marie Pédrot
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2012-06-12Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.ppedrot
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