From 9655b03d8d3f2b256b6ba71eb4b48bd767d4974b Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 27 Oct 2014 11:41:49 +0100
Subject: 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).
---
 stm/stm.ml                | 6 +++---
 toplevel/vernacentries.ml | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index 78f7682a39..64cf9bad72 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1513,7 +1513,8 @@ end = struct
           let id = VCS.get_branch_pos (VCS.current_branch ()) in
           let oid = fold_until (fun n (id,_,_) ->
             if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in
-          if n = 1 && !Flags.coqtop_ui && not !Flags.batch_mode then
+          if n = 1 && !Flags.coqtop_ui && not !Flags.batch_mode &&
+             not !Flags.print_emacs then
            VtStm (VtBack oid, false), VtNow
           else VtStm (VtBack oid, true), VtLater
       | VernacUndoTo _
@@ -1746,8 +1747,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
           prerr_endline ("undo to state " ^ Stateid.to_string id);
           Backtrack.backto id;
           VCS.checkout_shallowest_proof_branch ();
-          Reach.known_state ~cache:(interactive ()) id;
-          Pp.msg_notice (pr_open_cur_subgoals ()); `Ok
+          Reach.known_state ~cache:(interactive ()) id; `Ok
       | VtStm (VtBack id, false), VtLater ->
           anomaly(str"classifier: VtBack + VtLater must imply part_of_script")
 
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
-- 
cgit v1.2.3