idtacコマンドが成功した後にのみ、Ltac でメッセージを (? を使用して) 出力する方法はありますか? 何かのようなもの
first [ a; idtac "a did it!" | b; idtac "b did!" | idtac "nope"; fail ]
これは、複数のサブゴールによって複数のメッセージが出力されることを除いて、ほとんど機能します。
Goal True /\ True.
split; idtac "Split did it!".
最初の目標だけでフィルタリングするとうまくいくようです...
Goal True /\ True.
split; [ idtac "Split did it!" | .. ].
...そうでない場合を除いて：
Goal True /\ True.
tauto; [ idtac "Tauto did it!" | .. ].
おそらく両方のパターンを 1 つに組み合わせることができますが、100% のペナルティ ヒットにはあまり熱心ではありません。それでも、目標を完全に達成する戦術のケースは解決されません。
(私は主に 8.5 より前の Coq に対する回答に関心があります。8.5Infoなどではこれに適した機能が提供されているためです。それでも 8.5 であっても、特定の時点でのみデバッグ メッセージを出力できると興味深いでしょう)