[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.

1 files changed, 7 insertions, 8 deletions

diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index f5c6ab879..d2e014e55 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -148,12 +148,12 @@ let rec e_trivial_fail_db db_list local_db =
   let tacl =
     registered_e_assumption ::
     (Tacticals.New.tclTHEN Tactics.intro next) ::
-    (List.map fst (e_trivial_resolve (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_concl gl)))
+    (List.map fst (e_trivial_resolve (Tacmach.New.pf_env gl) (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_concl gl)))
   in
   Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl)
   end
 
-and e_my_find_search sigma db_list local_db secvars hdc concl =
+and e_my_find_search env sigma db_list local_db secvars hdc concl =
   let hint_of_db = hintmap_of sigma secvars hdc concl in
   let hintl =
       List.map_append (fun db ->
@@ -178,20 +178,19 @@ and e_my_find_search sigma db_list local_db secvars hdc concl =
         | Extern tacast -> conclPattern concl p tacast
        in
        let tac = run_hint t tac in
-       let sigma, env = Pfedit.get_current_context () in
        (tac, lazy (pr_hint env sigma t)))
   in
   List.map tac_of_hint hintl
 
-and e_trivial_resolve sigma db_list local_db secvars gl =
+and e_trivial_resolve env sigma db_list local_db secvars gl =
   let hd = try Some (decompose_app_bound sigma gl) with Bound -> None in
-  try priority (e_my_find_search sigma db_list local_db secvars hd gl)
+  try priority (e_my_find_search env sigma db_list local_db secvars hd gl)
   with Not_found -> []
 
-let e_possible_resolve sigma db_list local_db secvars gl =
+let e_possible_resolve env sigma db_list local_db secvars gl =
   let hd = try Some (decompose_app_bound sigma gl) with Bound -> None in
   try List.map (fun (b, (tac, pp)) -> (tac, b, pp))
-               (e_my_find_search sigma db_list local_db secvars hd gl)
+               (e_my_find_search env sigma db_list local_db secvars hd gl)
   with Not_found -> []
 
 let find_first_goal gls =
@@ -291,7 +290,7 @@ module SearchProblem = struct
 	let l =
           let concl = Reductionops.nf_evar (project g) (pf_concl g) in
 	  filter_tactics s.tacres
-                         (e_possible_resolve (project g) s.dblist (List.hd s.localdb) secvars concl)
+                         (e_possible_resolve (pf_env g) (project g) s.dblist (List.hd s.localdb) secvars concl)
 	in
 	List.map
 	  (fun (lgls, cost, pp) ->