Merge PR #11498: [exn] Forbid raising in exn printers, make them return Pp.t option

Reviewed-by: ppedrot

2 files changed, 6 insertions, 5 deletions

diff --git a/tactics/declare.ml b/tactics/declare.ml
index ce2f3ec2c5..5655bdfd4d 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -24,10 +24,11 @@ exception AlreadyDeclared of (string option * Id.t)
 
 let _ = CErrors.register_handler (function
     | AlreadyDeclared (kind, id) ->
-      seq [ Pp.pr_opt_no_spc (fun s -> str s ++ spc ()) kind
-          ; Id.print id; str " already exists."]
+      Some
+        (seq [ Pp.pr_opt_no_spc (fun s -> str s ++ spc ()) kind
+             ; Id.print id; str " already exists."])
     | _ ->
-      raise CErrors.Unhandled)
+      None)
 
 module NamedDecl = Context.Named.Declaration
 
diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml
index 72204e1d24..dbabc4e4e0 100644
--- a/tactics/pfedit.ml
+++ b/tactics/pfedit.ml
@@ -26,8 +26,8 @@ let use_unification_heuristics () = !use_unification_heuristics_ref
 
 exception NoSuchGoal
 let () = CErrors.register_handler begin function
-  | NoSuchGoal -> Pp.(str "No such goal.")
-  | _ -> raise CErrors.Unhandled
+  | NoSuchGoal -> Some Pp.(str "No such goal.")
+  | _ -> None
 end
 
 let get_nth_V82_goal p i =