diff options
| -rw-r--r-- | ide/coqide.ml | 3 | ||||
| -rw-r--r-- | toplevel/ide_blob.ml | 8 |
2 files changed, 8 insertions, 3 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index d5450220ed..7e742b55d8 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -720,6 +720,7 @@ object(self) method show_goals_full = if not full_goal_done then + proof_view#buffer#set_text ""; begin let menu_callback = if !current.contextual_menus_on_goal then (fun s () -> ignore (self#insert_this_phrase_on_success @@ -978,6 +979,7 @@ object(self) (* backtrack Coq to the phrase preceding iterator [i] *) method backtrack_to_no_lock i = prerr_endline "Backtracking_to iter starts now."; + full_goal_done <- false; (* pop Coq commands until we reach iterator [i] *) let rec n_step n = if Stack.is_empty cmd_stack then n else @@ -1030,6 +1032,7 @@ object(self) else self#backtrack_to point method undo_last_step = + full_goal_done <- false; if Mutex.try_lock coq_may_stop then (push_info "Undoing last step..."; (try diff --git a/toplevel/ide_blob.ml b/toplevel/ide_blob.ml index d578122a0f..9dce5c1ccf 100644 --- a/toplevel/ide_blob.ml +++ b/toplevel/ide_blob.ml @@ -404,9 +404,10 @@ let concl_next_tac sigma concl = ]) let current_goals () = - let pfts = - Proof_global.give_me_the_proof () - in + try + let pfts = + Proof_global.give_me_the_proof () + in let { Evd.it=all_goals ; sigma=sigma } = Proof.V82.subgoals pfts in if all_goals = [] then begin @@ -441,6 +442,7 @@ let current_goals () = in Goals (List.map process_goal all_goals) end + with Proof_global.NoCurrentProof -> Message "" (* quick hack to have a clean message screen *) let id_of_name = function | Names.Anonymous -> id_of_string "x" |