aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/Tactics.v
AgeCommit message (Expand)Author
2020-11-29Fixing printing of apply in (continuation of #12246).Hugo Herbelin
2020-11-16Avoid exposing an internal names when "intros _ H" fails.Hugo Herbelin
2019-10-29`assert_succeeds`&`assert_fails`: multisuccess fixJason Gross
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