diff options
| author | Enrico Tassi | 2018-08-01 11:21:49 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-08-01 11:21:49 +0200 |
| commit | a257ddce0ef35b8596e71377e9a1967baefebea4 (patch) | |
| tree | 0a7865ccdd9e18eceefa6e3773af51e152f4005f /toplevel | |
| parent | e8dbb311c82acb5cdf6d2f81dd6a1df503a7a123 (diff) | |
| parent | 7d2a9df50d519607c23a97c8973cb7d026d3d8d0 (diff) | |
Merge PR #8182: Handle diffs better for the "Undo" command.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqloop.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 7b7e1b16c0..9e16b97608 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -376,7 +376,8 @@ let rec vernac_loop ~state = else (Feedback.msg_warning (str "There is no ML toplevel."); vernac_loop ~state) | {v=VernacControl c; loc} -> let nstate = Vernac.process_expr ~state (make ?loc c) in - top_goal_print state.proof nstate.proof; + let dproof = Stm.get_prev_proof ~doc:state.doc (Stm.get_current_state ~doc:state.doc) in + top_goal_print dproof nstate.proof; vernac_loop ~state:nstate with | Stm.End_of_input -> |