diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/declare.ml | 2 | ||||
| -rw-r--r-- | vernac/himsg.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/vernac/declare.ml b/vernac/declare.ml index 6326a22e83..85359d5b62 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -2206,7 +2206,7 @@ let solve_by_tac ?loc name evi t ~poly ~uctx = Inductiveops.control_only_guard env (Evd.from_ctx uctx) (EConstr.of_constr body); Some (body, types, uctx) with - | Refiner.FailError (_, s) as exn -> + | Tacticals.FailError (_, s) as exn -> let _ = Exninfo.capture exn in CErrors.user_err ?loc ~hdr:"solve_obligation" (Lazy.force s) (* If the proof is open we absorb the error and leave the obligation open *) diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 9d67ce3757..79f11fd6bc 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1398,7 +1398,7 @@ let rec vernac_interp_error_handler = function str "The reference" ++ spc () ++ Libnames.pr_qualid q ++ spc () ++ str "was not found" ++ spc () ++ str "in the current" ++ spc () ++ str "environment." - | Refiner.FailError (i,s) -> + | Tacticals.FailError (i,s) -> let s = Lazy.force s in str "Tactic failure" ++ (if Pp.ismt s then s else str ": " ++ s) ++ |