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

5 files changed, 52 insertions, 46 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index cee6d4bea..9e4d132d4 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -376,7 +376,7 @@ let rec e_trivial_fail_db only_classes db_list local_db secvars =
     Proofview.Goal.enter
     begin fun gl ->
     let tacs = e_trivial_resolve db_list local_db secvars only_classes
-                                 (project gl) (pf_concl gl) in
+                                 (pf_env gl) (project gl) (pf_concl gl) in
       tclFIRST (List.map (fun (x,_,_,_,_) -> x) tacs)
     end
   in
@@ -386,7 +386,7 @@ let rec e_trivial_fail_db only_classes db_list local_db secvars =
   in
   tclFIRST (List.map tclCOMPLETE tacl)
 
-and e_my_find_search db_list local_db secvars hdc complete only_classes sigma concl =
+and e_my_find_search db_list local_db secvars hdc complete only_classes env sigma concl =
   let open Proofview.Notations in
   let prods, concl = EConstr.decompose_prod_assum sigma concl in
   let nprods = List.length prods in
@@ -464,7 +464,6 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co
       in
       let tac = run_hint t tac in
       let tac = if complete then Tacticals.New.tclCOMPLETE tac else tac in
-      let _, env = Pfedit.get_current_context () in
       let pp =
         match p with
         | Some pat when get_typeclasses_filtered_unification () ->
@@ -476,16 +475,16 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co
         | _ -> (tac, b, false, name, lazy (pr_hint env sigma t ++ pp))
   in List.map tac_of_hint hintl
 
-and e_trivial_resolve db_list local_db secvars only_classes sigma concl =
+and e_trivial_resolve db_list local_db secvars only_classes env sigma concl =
   let hd = try Some (decompose_app_bound sigma concl) with Bound -> None in
   try
-    e_my_find_search db_list local_db secvars hd true only_classes sigma concl
+    e_my_find_search db_list local_db secvars hd true only_classes env sigma concl
   with Not_found -> []
 
-let e_possible_resolve db_list local_db secvars only_classes sigma concl =
+let e_possible_resolve db_list local_db secvars only_classes env sigma concl =
   let hd = try Some (decompose_app_bound sigma concl) with Bound -> None in
   try
-    e_my_find_search db_list local_db secvars hd false only_classes sigma concl
+    e_my_find_search db_list local_db secvars hd false only_classes env sigma concl
   with Not_found -> []
 
 let cut_of_hints h =
@@ -719,7 +718,7 @@ module V85 = struct
     let concl = Goal.V82.concl s gl in
     let tacgl = {it = gl; sigma = s;} in
     let secvars = secvars_of_hyps (Environ.named_context_of_val (Goal.V82.hyps s gl)) in
-    let poss = e_possible_resolve hints info.hints secvars info.only_classes s concl in
+    let poss = e_possible_resolve hints info.hints secvars info.only_classes env s concl in
     let unique = is_unique env s concl in
     let rec aux i foundone = function
       | (tac, _, extern, name, pp) :: tl ->
@@ -1072,7 +1071,7 @@ module Search = struct
             else str" without backtracking"));
     let secvars = compute_secvars gl in
     let poss =
-      e_possible_resolve hints info.search_hints secvars info.search_only_classes sigma concl in
+      e_possible_resolve hints info.search_hints secvars info.search_only_classes env sigma concl in
     (* If no goal depends on the solution of this one or the
        instances are irrelevant/assumed to be unique, then
        we don't need to backtrack, as long as no evar appears in the goal
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) ->
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 0d6263246..22073d39b 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1436,8 +1436,9 @@ let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
 	(tac (clenv_value eq_clause))
 
 let get_previous_hyp_position id gl =
+  let env, sigma = Proofview.Goal.(env gl, sigma gl) in
   let rec aux dest = function
-  | [] -> raise (RefinerError (NoSuchHyp id))
+  | [] -> raise (RefinerError (env, sigma, NoSuchHyp id))
   | d :: right ->
     let hyp = Context.Named.Declaration.get_id d in
     if Id.equal hyp id then dest else aux (MoveAfter hyp) right
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 70e84013b..7f9b5ef34 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1400,15 +1400,10 @@ let pr_hint env sigma h = match h.obj with
   | Give_exact (c, _) -> (str"exact " ++ pr_hint_elt env sigma c)
   | Res_pf_THEN_trivial_fail (c, _) ->
       (str"simple apply " ++ pr_hint_elt env sigma c ++ str" ; trivial")
-  | Unfold_nth c -> (str"unfold " ++  pr_evaluable_reference c)
+  | Unfold_nth c ->
+    str"unfold " ++  pr_evaluable_reference c
   | Extern tac ->
-      let env =
-        try
-          let (_, env) = Pfedit.get_current_goal_context () in
-          env
-        with e when CErrors.noncritical e -> Global.env ()
-      in
-      (str "(*external*) " ++ Pputils.pr_glb_generic env tac)
+    str "(*external*) " ++ Pputils.pr_glb_generic env tac
 
 let pr_id_hint env sigma (id, v) =
   let pr_pat p = str", pattern " ++ pr_lconstr_pattern_env env sigma p in
@@ -1507,6 +1502,7 @@ let pr_hint_db_env env sigma db =
   hov 2 (str"Cut: " ++ pp_hints_path (Hint_db.cut db)) ++ fnl () ++
   content
 
+(* Deprecated in the mli *)
 let pr_hint_db db =
   let sigma, env = Pfedit.get_current_context () in
   pr_hint_db_env env sigma db
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e072bd95f..6aa052d32 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -187,7 +187,7 @@ let introduction ?(check=true) id =
     match EConstr.kind sigma concl with
     | Prod (_, t, b) -> unsafe_intro env store (LocalAssum (id, t)) b
     | LetIn (_, c, t, b) -> unsafe_intro env store (LocalDef (id, c, t)) b
-    | _ -> raise (RefinerError IntroNeedsProduct)
+    | _ -> raise (RefinerError (env, sigma, IntroNeedsProduct))
   end
 
 let refine          = Tacmach.refine
@@ -319,7 +319,7 @@ let move_hyp id dest =
     let ty = Proofview.Goal.concl gl in
     let store = Proofview.Goal.extra gl in
     let sign = named_context_val env in
-    let sign' = move_hyp_in_named_context sigma id dest sign in
+    let sign' = move_hyp_in_named_context env sigma id dest sign in
     let env = reset_with_named_context sign' env in
     Refine.refine ~typecheck:false begin fun sigma ->
       Evarutil.new_evar env sigma ~principal:true ~store ty
@@ -348,13 +348,15 @@ let rename_hyp repl =
       let hyps = Proofview.Goal.hyps gl in
       let concl = Proofview.Goal.concl gl in
       let store = Proofview.Goal.extra gl in
+      let env = Proofview.Goal.env gl in
+      let sigma = Proofview.Goal.sigma gl in
       (** Check that we do not mess variables *)
       let fold accu decl = Id.Set.add (NamedDecl.get_id decl) accu in
       let vars = List.fold_left fold Id.Set.empty hyps in
       let () =
         if not (Id.Set.subset src vars) then
           let hyp = Id.Set.choose (Id.Set.diff src vars) in
-          raise (RefinerError (NoSuchHyp hyp))
+          raise (RefinerError (env, sigma, NoSuchHyp hyp))
       in
       let mods = Id.Set.diff vars src in
       let () =
@@ -442,9 +444,9 @@ let find_name mayrepl decl naming gl = match naming with
 (*   Computing position of hypotheses for replacing           *)
 (**************************************************************)
 
-let get_next_hyp_position id =
+let get_next_hyp_position env sigma id =
   let rec aux = function
-  | [] -> error_no_such_hypothesis id
+  | [] -> error_no_such_hypothesis env sigma id
   | decl :: right ->
     if Id.equal (NamedDecl.get_id decl) id then
       match right with decl::_ -> MoveBefore (NamedDecl.get_id decl) | [] -> MoveFirst
@@ -453,9 +455,9 @@ let get_next_hyp_position id =
   in
   aux
 
-let get_previous_hyp_position id =
+let get_previous_hyp_position env sigma id =
   let rec aux dest = function
-  | [] -> error_no_such_hypothesis id
+  | [] -> error_no_such_hypothesis env sigma id
   | decl :: right ->
       let hyp = NamedDecl.get_id decl in
       if Id.equal hyp id then dest else aux (MoveAfter hyp) right
@@ -483,7 +485,7 @@ let internal_cut_gen ?(check=true) dir replace id t =
     let sign = named_context_val env in
     let sign',t,concl,sigma =
       if replace then
-        let nexthyp = get_next_hyp_position id (named_context_of_val sign) in
+        let nexthyp = get_next_hyp_position env sigma id (named_context_of_val sign) in
         let sign',t,concl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in
         let sign' = insert_decl_in_named_context sigma (LocalAssum (id,t)) nexthyp sign' in
         sign',t,concl,sigma
@@ -1000,6 +1002,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
   let open Context.Rel.Declaration in
   Proofview.Goal.enter begin fun gl ->
     let sigma = Tacmach.New.project gl in
+    let env = Tacmach.New.pf_env gl in
     let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
     match EConstr.kind sigma concl with
     | Prod (name,t,u) when not dep_flag || not (noccurn sigma 1 u) ->
@@ -1009,7 +1012,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
         let name = find_name false (LocalDef (name,b,t)) name_flag gl in
 	build_intro_tac name move_flag tac
     | _ ->
-	begin if not force_flag then Proofview.tclZERO (RefinerError IntroNeedsProduct)
+        begin if not force_flag then Proofview.tclZERO (RefinerError (env, sigma, IntroNeedsProduct))
             (* Note: red_in_concl includes betaiotazeta and this was like *)
             (* this since at least V6.3 (a pity *)
             (* that intro do betaiotazeta only when reduction is needed; and *)
@@ -1020,7 +1023,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
 	  (Tacticals.New.tclTHEN hnf_in_concl
 	     (intro_then_gen name_flag move_flag false dep_flag tac))
           begin function (e, info) -> match e with
-            | RefinerError IntroNeedsProduct ->
+            | RefinerError (env, sigma, IntroNeedsProduct) ->
                 Tacticals.New.tclZEROMSG (str "No product even after head-reduction.")
             | e -> Proofview.tclZERO ~info e
           end
@@ -1059,7 +1062,7 @@ let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac =
          (fun id -> aux (n+1) (id::ids))
       end
       begin function (e, info) -> match e with
-      | RefinerError IntroNeedsProduct ->
+      | RefinerError (env, sigma, IntroNeedsProduct) ->
           tac ids
       | e -> Proofview.tclZERO ~info e
       end
@@ -1070,8 +1073,9 @@ let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac =
 
 let intro_replacing id =
   Proofview.Goal.enter begin fun gl ->
+  let env, sigma = Proofview.Goal.(env gl, sigma gl) in
   let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
-  let next_hyp = get_next_hyp_position id hyps in
+  let next_hyp = get_next_hyp_position env sigma id hyps in
   Tacticals.New.tclTHENLIST [
     clear_for_replacing [id];
     introduction id;
@@ -1090,8 +1094,9 @@ let intro_replacing id =
 let intros_possibly_replacing ids =
   let suboptimal = true in
   Proofview.Goal.enter begin fun gl ->
+    let env, sigma = Proofview.Goal.(env gl, sigma gl) in
     let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
-    let posl = List.map (fun id -> (id, get_next_hyp_position id hyps)) ids in
+    let posl = List.map (fun id -> (id, get_next_hyp_position env sigma id hyps)) ids in
     Tacticals.New.tclTHEN
       (Tacticals.New.tclMAP (fun id -> 
 	Tacticals.New.tclTRY (clear_for_replacing [id]))
@@ -1105,7 +1110,8 @@ let intros_possibly_replacing ids =
 let intros_replacing ids =
   Proofview.Goal.enter begin fun gl ->
     let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
-    let posl = List.map (fun id -> (id, get_next_hyp_position id hyps)) ids in
+    let env, sigma = Proofview.Goal.(env gl, sigma gl) in
+    let posl = List.map (fun id -> (id, get_next_hyp_position env sigma id hyps)) ids in
     Tacticals.New.tclTHEN
       (clear_for_replacing ids)
       (Tacticals.New.tclMAP (fun (id,pos) -> intro_move (Some id) pos) posl)
@@ -2633,8 +2639,10 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars
   Proofview.Goal.enter begin fun gl ->
   let destopt =
     if with_evars then MoveLast (* evars would depend on the whole context *)
-    else
-      get_previous_hyp_position id (Proofview.Goal.hyps (Proofview.Goal.assume gl)) in
+    else (
+      let env, sigma = Proofview.Goal.(env gl, sigma gl) in
+      get_previous_hyp_position env sigma id (Proofview.Goal.hyps (Proofview.Goal.assume gl))
+    ) in
   let naming,ipat_tac =
     prepare_intros_opt with_evars (IntroIdentifier id) destopt ipat in
   let lemmas_target, last_lemma_target =
@@ -4448,8 +4456,11 @@ let check_enough_applied env sigma elim =
           check_expected_type env sigma elimc elimt
 
 let guard_no_unifiable = Proofview.guard_no_unifiable >>= function
-| None -> Proofview.tclUNIT ()
-| Some l -> Proofview.tclZERO (RefinerError (UnresolvedBindings l))
+  | None -> Proofview.tclUNIT ()
+  | Some l ->
+    Proofview.tclENV     >>= function env ->
+    Proofview.tclEVARMAP >>= function sigma ->
+    Proofview.tclZERO (RefinerError (env, sigma, UnresolvedBindings l))
 
 let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
      id ((pending,(c0,lbind)),(eqname,names)) t0 inhyps cls tac =
@@ -4648,7 +4659,7 @@ let induction_destruct isrec with_evars (lc,elim) =
         (Tacticals.New.tclMAP (fun (a,b,cl) ->
           Proofview.Goal.enter begin fun gl ->
           let env = Proofview.Goal.env gl in
-          let sigma = Tacmach.New.project gl in      
+          let sigma = Tacmach.New.project gl in
           onOpenInductionArg env sigma (fun clear_flag a ->
             induction_gen clear_flag false with_evars None (a,b) cl) a
           end) l)
@@ -4673,7 +4684,7 @@ let induction_destruct isrec with_evars (lc,elim) =
     end
 
 let induction ev clr c l e =
-  induction_gen clr true ev e 
+  induction_gen clr true ev e
     ((Evd.empty,(c,NoBindings)),(None,l)) None
 
 let destruct ev clr c l e =