aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/Tactics.v
AgeCommit message (Expand)Author
2018-10-04test-suite: cleaningVincent Laporte
2017-10-19Moving bug numbers to BZ# format in the test-suite.Théo Zimmermann
2017-05-17A fix for #5390 (a useful error on used introduction names was masked).Hugo Herbelin
2011-12-17Bypassing the use of (currently unimplemented) "Show Script" in testsherbelin
2006-04-24Timide tentative de clarification du statut de l'opérateur de filtrageherbelin
2005-12-23Test printing of Tactic Notation which was broken until dec 2005herbelin