Merge branch 'v8.5'

4 files changed, 8 insertions, 9 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 11621078d..6d44ca59e 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -227,7 +227,7 @@ type coqtop = {
   (* non quoted command-line arguments of coqtop *)
   mutable sup_args : string list;
   (* called whenever coqtop dies *)
-  mutable reset_handler : reset_kind -> unit task;
+  mutable reset_handler : unit task;
   (* called whenever coqtop sends a feedback message *)
   mutable feedback_handler : Feedback.feedback -> unit;
   (* actual coqtop process and its status *)
@@ -421,6 +421,7 @@ let mkready coqtop =
   fun () -> coqtop.status <- Ready; Void
 
 let rec respawn_coqtop ?(why=Unexpected) coqtop =
+  if why = Unexpected then warning "Coqtop died badly. Resetting.";
   clear_handle coqtop.handle;
   ignore_error (fun () ->
      coqtop.handle <-
@@ -432,7 +433,7 @@ let rec respawn_coqtop ?(why=Unexpected) coqtop =
      If not, there isn't much we can do ... *)
   assert (coqtop.handle.alive = true);
   coqtop.status <- New;
-  ignore (coqtop.reset_handler why coqtop.handle (mkready coqtop))
+  ignore (coqtop.reset_handler coqtop.handle (mkready coqtop))
 
 let spawn_coqtop sup_args =
   bind_self_as (fun this -> {
@@ -440,7 +441,7 @@ let spawn_coqtop sup_args =
                (fun () -> respawn_coqtop (this ()))
                (fun msg -> (this ()).feedback_handler msg);
     sup_args = sup_args;
-    reset_handler = (fun _ _ k -> k ());
+    reset_handler = (fun _ k -> k ());
     feedback_handler = (fun _ -> ());
     status = New;
   })
diff --git a/ide/coq.mli b/ide/coq.mli
index 7cef6a4d0..8a1fa3ed1 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -60,7 +60,7 @@ val is_computing : coqtop -> bool
 val spawn_coqtop : string list -> coqtop
 (** Create a coqtop process with some command-line arguments. *)
 
-val set_reset_handler : coqtop -> (reset_kind -> unit task) -> unit
+val set_reset_handler : coqtop -> unit task -> unit
 (** Register a handler called when a coqtop dies (badly or on purpose) *)
 
 val set_feedback_handler : coqtop -> (Feedback.feedback -> unit) -> unit
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
diff --git a/ide/coqOps.mli b/ide/coqOps.mli
index 4a37a1fa5..332c18f2f 100644
--- a/ide/coqOps.mli
+++ b/ide/coqOps.mli
@@ -15,7 +15,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