diff options
| author | Jim Fehrle | 2019-06-08 05:04:41 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2019-06-25 12:45:03 -0700 |
| commit | 403917b7d9ecb2ddfaaac2185c355d415d5fa5bc (patch) | |
| tree | e5afcff136068558ac11b7643709be9a7710ebd5 /toplevel/coqloop.ml | |
| parent | 7dfcb0f7c817e66280ab37b6c653b5596a16c249 (diff) | |
Re-add the "Show Goal" command for Prooftree in PG.
It prints a goal given its internal goal id and the Stm state id.
Diffstat (limited to 'toplevel/coqloop.ml')
| -rw-r--r-- | toplevel/coqloop.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 4077c02604..4bcde566e3 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -403,6 +403,11 @@ let rec vernac_loop ~state = top_goal_print ~doc:state.doc c state.proof nstate.proof; vernac_loop ~state:nstate + | Some (VernacShowGoal {gid; sid}) -> + let proof = Stm.get_proof ~doc:state.doc (Stateid.of_int sid) in + Feedback.msg_notice (Printer.pr_goal_emacs ~proof gid sid); + vernac_loop ~state + | None -> top_stderr (fnl ()); exit 0 |