diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2015-10-06 13:38:15 +0200 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2015-10-06 13:38:15 +0200 |
| commit | 840155eafd9607c7656c80770de1e2819fe56a13 (patch) | |
| tree | 6b4878d586fa611d4e85068d8e4a9eef2e9882e5 /engine/logic_monad.ml | |
| parent | df9caebb04fb681ec66b79c41ae01918cd2336de (diff) | |
Fixing emacs output in debugging mode.
Goal displaying during Debugging ltac is a notice message now. Other
messages are debug messages. This does not change anything in coqide
or coqtop, but allows proofgeneral to dispatch them in the right
buffers (pg had to be fixed too).
Diffstat (limited to 'engine/logic_monad.ml')
0 files changed, 0 insertions, 0 deletions