diff options
| author | vgross | 2010-07-05 17:39:51 +0000 |
|---|---|---|
| committer | vgross | 2010-07-05 17:39:51 +0000 |
| commit | d4af7ddf3585f6938ae24b72661965b1a00972ea (patch) | |
| tree | 0447793d6e8bd17d95f6110f1ca05edb8f8d224f /ide | |
| parent | a90ccfa5f25858e8cb224b4cfa4f724ca84e3ea4 (diff) | |
Fix goal display when backtracking
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13246 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqide.ml | 3 |
1 files changed, 3 insertions, 0 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 |