diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-27 20:47:43 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-27 20:47:43 +0200 |
| commit | 663a8647bbc32e11243091de80f9953ed5fb7eff (patch) | |
| tree | 7fba0a308daee7586221f752e233dd8fa9c8f5f5 /ide/coqOps.ml | |
| parent | d4725f692a5f202ca4c5d6341b586b0e377f6973 (diff) | |
| parent | a7ea32fbf3829d1ce39ce9cc24b71791727090c5 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'ide/coqOps.ml')
| -rw-r--r-- | ide/coqOps.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml index c912adcf1..f0e767cba 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -136,7 +136,7 @@ object method tactic_wizard : string list -> unit task method process_next_phrase : unit task method process_until_end_or_error : unit task - method handle_reset_initial : Coq.reset_kind -> unit task + method handle_reset_initial : unit task method raw_coq_query : string -> unit task method show_goals : unit task method backtrack_last_phrase : unit task @@ -844,10 +844,8 @@ object(self) in loop l - method handle_reset_initial why = + method handle_reset_initial = let action () = - if why = Coq.Unexpected then warning "Coqtop died badly. Resetting." - else (* clear the stack *) if Doc.focused document then Doc.unfocus document; while not (Doc.is_empty document) do |