diff options
| author | Enrico Tassi | 2014-10-22 15:12:51 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-10-22 16:00:01 +0200 |
| commit | ad28bacca8cf9f779db099f7c42938b96ae31f42 (patch) | |
| tree | f0cceec16fc36bfa586bad7b0a0536215527ce5d /kernel | |
| parent | 356597ffc42b9298e27e0af2cfd05fe73f6d1383 (diff) | |
Goal printing made uniform: always done in STM (close 3585)
Goal printing was partially broken. Some commands in vernacentries
were printing, but not all of them. Moreover an unlucky combination
of `Flags.verbosely (fun () -> interp "Set Silent")` was making the
silent flag not settable anymore.
Now STM always print the open goals after a command when run in interactive
mode via coqtop or emacs. More modern GUI do ask for the goals.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions