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 /toplevel | |
| 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 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index e04cad5c4a..90689aee6f 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1686,7 +1686,7 @@ let vernac_bullet (bullet:Proof_global.Bullet.t) = let vernac_show = function | ShowGoal goalref -> let info = match goalref with - | OpenSubgoals -> pr_open_subgoals () + | OpenSubgoals -> mt() (* the STM prints it *) | NthGoal n -> pr_nth_open_subgoal n | GoalId id -> pr_goal_by_id id in |