3 files changed, 18 insertions, 16 deletions
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index 3c383b2e00..1caf2c2722 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -38,9 +38,9 @@ exception Tac_Timeout
 exception TacticFailure of exn
 
 let _ = CErrors.register_handler begin function
-  | Exception e -> CErrors.print e
-  | TacticFailure e -> CErrors.print e
-  | _ -> raise CErrors.Unhandled
+  | Exception e -> Some (CErrors.print e)
+  | TacticFailure e -> Some (CErrors.print e)
+  | _ -> None
 end
 
 (** {6 Non-logical layer} *)
@@ -83,7 +83,7 @@ struct
 
   (** [Pervasives.raise]. Except that exceptions are wrapped with
       {!Exception}. *)
-  let raise ?info = fun e -> (); fun () -> Exninfo.raise ?info (Exception e)
+  let raise (e, info) () = Exninfo.iraise (Exception e, info)
 
   (** [try ... with ...] but restricted to {!Exception}. *)
   let catch = fun s h -> ();
@@ -93,7 +93,8 @@ struct
         h (e, info) ()
 
   let read_line = fun () -> try read_line () with e ->
-    let (e, info) = CErrors.push e in raise ~info e ()
+    let (e, info) = CErrors.push e in
+    raise (e, info) ()
 
   let print_char = fun c -> (); fun () -> print_char c
 
diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli
index 75920455ce..5002d24af0 100644
--- a/engine/logic_monad.mli
+++ b/engine/logic_monad.mli
@@ -70,7 +70,7 @@ module NonLogical : sig
 
   (** [Pervasives.raise]. Except that exceptions are wrapped with
       {!Exception}. *)
-  val raise : ?info:Exninfo.info -> exn -> 'a t
+  val raise : Exninfo.iexn -> 'a t
 
   (** [try ... with ...] but restricted to {!Exception}. *)
   val catch : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t
diff --git a/engine/proofview.ml b/engine/proofview.ml
index b0ea75ac60..a26ce71141 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -303,8 +303,8 @@ let tclONCE = Proof.once
 exception MoreThanOneSuccess
 let _ = CErrors.register_handler begin function
   | MoreThanOneSuccess ->
-    Pp.str "This tactic has more than one success."
-  | _ -> raise CErrors.Unhandled
+    Some (Pp.str "This tactic has more than one success.")
+  | _ -> None
 end
 
 (** [tclEXACTLY_ONCE e t] succeeds as [t] if [t] has exactly one
@@ -348,8 +348,8 @@ exception NoSuchGoals of int
 
 let _ = CErrors.register_handler begin function
   | NoSuchGoals n ->
-    str "No such " ++ str (String.plural n "goal") ++ str "."
-  | _ -> raise CErrors.Unhandled
+    Some (str "No such " ++ str (String.plural n "goal") ++ str ".")
+  | _ -> None
 end
 
 (** [tclFOCUS ?nosuchgoal i j t] applies [t] in a context where
@@ -421,9 +421,10 @@ exception SizeMismatch of int*int
 let _ = CErrors.register_handler begin function
   | SizeMismatch (i,j) ->
     let open Pp in
-    str"Incorrect number of goals" ++ spc() ++
-    str"(expected "++int i++str(String.plural i " tactic") ++ str", was given "++ int j++str")."
-  | _ -> raise CErrors.Unhandled
+    Some (
+      str"Incorrect number of goals" ++ spc() ++
+      str"(expected "++int i++str(String.plural i " tactic") ++ str", was given "++ int j++str").")
+  | _ -> None
 end
 
 (** A variant of [Monad.List.iter] where we iter over the focused list
@@ -908,8 +909,8 @@ let tclPROGRESS t =
 
 let _ = CErrors.register_handler begin function
   | Logic_monad.Tac_Timeout ->
-    Pp.str "[Proofview.tclTIMEOUT] Tactic timeout!"
-  | _ -> raise CErrors.Unhandled
+    Some (Pp.str "[Proofview.tclTIMEOUT] Tactic timeout!")
+  | _ -> None
 end
 
 let tclTIMEOUT n t =
@@ -937,7 +938,7 @@ let tclTIMEOUT n t =
           return (Util.Inr (Logic_monad.Tac_Timeout, info))
         | Logic_monad.TacticFailure e ->
           return (Util.Inr (e, info))
-        | e -> Logic_monad.NonLogical.raise ~info e
+        | e -> Logic_monad.NonLogical.raise (e, info)
       end
   end >>= function
     | Util.Inl (res,s,m,i) ->