From 34f63d7d890921cce37f4d48f48cdb020f2ac988 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 26 Nov 2017 19:00:46 +0100 Subject: [proof] Embed evar_map in RefinerError exception. The exception needs to carry aroud a pair of `env, sigma` so printing is correct. This gets rid of a few global calls, and it is IMO the right thing to do. While we are at it, we incorporate some fixes to a couple of additional printing functions missing the `env, sigma` pair. --- vernac/explainErr.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'vernac/explainErr.ml') 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 -- cgit v1.2.3