diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/declare.ml | 7 | ||||
| -rw-r--r-- | tactics/pfedit.ml | 4 |
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 = |