diff options
| author | Arnaud Spiwack | 2014-08-05 16:13:33 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-08-05 16:56:20 +0200 |
| commit | afa441019432f70245fed6adc5eb0318514e4357 (patch) | |
| tree | 822bf107f1e1b7dec8a6857e086e6f2996b67b96 /plugins | |
| parent | 5b92ff7b0a641bf2daa31b60bf49b57a5d1e8452 (diff) | |
Ltac's [idtac] is now interpreted outside of a goal if possible.
It avoids printing several times the same things when no constr are involved in the message. It also allows to print messages even after all goals have been solved.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions