diff options
| author | Pierre-Marie Pédrot | 2020-06-26 12:50:46 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-06-29 15:20:35 +0200 |
| commit | d28af587b9848c6155c7eae482591836f0fbc68f (patch) | |
| tree | f485f9cd2c05bd05d2b02c832fe732f1419004e0 /vernac | |
| parent | f34dcb97406611704c93970ea623d6a8587e5ba8 (diff) | |
Move the FailError exception from Refiner to Tacticals.
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) ++ |