diff options
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 |