aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/Tactics.out
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
2017-05-17A fix for #5390 (a useful error on used introduction names was masked).Hugo Herbelin
2016-12-02Fix test-suite after change in "context" printing.Maxime Dénès
2011-12-17Bypassing the use of (currently unimplemented) "Show Script" in testsherbelin
2008-08-04Évolutions diverses et variées.herbelin
2008-01-22Ajout de sauts de ligne dans l'affichage des scripts (cf commit 10445)notin
2006-10-13Correction test-suite suite à r9186notin
2006-09-25Corrections mineuresnotin
2006-06-09Adaptation Tactics.out et Cases.out au comportement actuel à défaut d'évit...herbelin
2006-05-10Conformité nouveaux principes: Declare Module non utilisable pour définir u...herbelin
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