diff options
| author | Jim Fehrle | 2018-07-07 21:17:32 -0400 |
|---|---|---|
| committer | Jim Fehrle | 2018-07-31 16:32:42 -0700 |
| commit | 7d2a9df50d519607c23a97c8973cb7d026d3d8d0 (patch) | |
| tree | b4194c9684b7e249fd712ecb4edfc135193a18a5 /toplevel | |
| parent | e130be4ccb68e0876ed789d295ae9a94d4358bf9 (diff) | |
Code to handle "Back" command for diffs.
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 -> |