diff options
| author | Emilio Jesus Gallego Arias | 2020-01-30 23:36:19 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-01-30 23:36:19 +0100 |
| commit | 173a2d8b0fba1a85b618654151af04b5decf9bac (patch) | |
| tree | 8f7385dbc348bed11568414729ec4e1f65a295e4 /tactics | |
| parent | 869f731439b7fe034067bb550b60713b9b790f5b (diff) | |
[exn] Don't reraise in exception printers
This behaviour seems a bit dubious and it is indeed not needed, also
such re-raises seem like they will mess with the backtrace.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/pfedit.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml index 3c9803432a..a4a06873b8 100644 --- a/tactics/pfedit.ml +++ b/tactics/pfedit.ml @@ -27,7 +27,7 @@ let use_unification_heuristics () = !use_unification_heuristics_ref exception NoSuchGoal let () = CErrors.register_handler begin function - | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.") + | NoSuchGoal -> Pp.(str "No such goal.") | _ -> raise CErrors.Unhandled end |