diff options
| author | Emilio Jesus Gallego Arias | 2020-06-30 15:57:33 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-30 15:57:33 +0200 |
| commit | 9c9330f2e3a5ff205973881003c5734034b7d0d5 (patch) | |
| tree | ba410bd04083fe3f8bf6a0f70fb4a1fa66663115 /vernac | |
| parent | bffe3e8dcbb6019b30d32081f0b56eba30bf8be7 (diff) | |
| parent | 6bb0c6df0dd331b8acb78a720eaf076aea5fce47 (diff) | |
Merge PR #12599: Remove the Refiner module
Reviewed-by: ejgallego
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 540d470fdc..0c4f76f682 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) ++ |