diff options
Diffstat (limited to 'vernac/explainErr.ml')
| -rw-r--r-- | vernac/explainErr.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index 3a8e8fb43..d328ad0cf 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -75,8 +75,7 @@ let process_vernac_interp_error exn = match fst exn with wrap_vernac_error exn (Himsg.explain_pattern_matching_error env sigma e) | Tacred.ReductionTacticError e -> wrap_vernac_error exn (Himsg.explain_reduction_tactic_error e) - | Logic.RefinerError e -> - let sigma, env = Pfedit.get_current_context () in + | Logic.RefinerError (env, sigma, e) -> wrap_vernac_error exn (Himsg.explain_refiner_error env sigma e) | Nametab.GlobalizationError q -> wrap_vernac_error exn |