diff options
| author | Pierre-Marie Pédrot | 2020-02-03 09:18:41 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-03 09:18:41 +0100 |
| commit | 0ffd145a082f69aeb3980717f501d5c1c503a996 (patch) | |
| tree | 6e5cad60e5d7fa31b03d975f59367411bfd254b9 /tactics | |
| parent | e5da14f87fea2e99b5e4e70dc6340f40daaef41f (diff) | |
| parent | 173a2d8b0fba1a85b618654151af04b5decf9bac (diff) | |
Merge PR #11490: [exn] Don't reraise in exception printers
Ack-by: aspiwack
Reviewed-by: ppedrot
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 |