diff options
| author | Enrico Tassi | 2014-10-27 11:41:49 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-10-27 11:41:49 +0100 |
| commit | 9655b03d8d3f2b256b6ba71eb4b48bd767d4974b (patch) | |
| tree | 6899a28dfac21a8bce3c1171019baaf1deb6cd7f /dev/tools/objects.el | |
| parent | b56ec63bf021a8dd95ce2eddc365115ce818a43e (diff) | |
Fixes for PG (Close 3763, 3770)
- Show does not print the goal twice
- Undo is considered as part of the document when PG mode
(bug introduced when Undo was said not to be part of the document in
coqtop mode).
Diffstat (limited to 'dev/tools/objects.el')
0 files changed, 0 insertions, 0 deletions