Merge PR #6251: [proof] Embed evar_map in RefinerError exception.

20 files changed, 124 insertions, 114 deletions

diff --git a/API/API.mli b/API/API.mli
index 3ed008ff5..c5a1743f7 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4801,7 +4801,7 @@ sig
   | IntroNeedsProduct
   | DoesNotOccurIn of Constr.t * Names.Id.t
   | NoSuchHyp of Names.Id.t
-  exception RefinerError of refiner_error
+  exception RefinerError of Environ.env * Evd.evar_map * refiner_error
   val catchable_exception : exn -> bool
 end
 
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index c0060c5a7..1f2e5f7ac 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -2021,14 +2021,16 @@ let add_morphism glob binders m s n =
 (** Taken from original setoid_replace, to emulate the old rewrite semantics where
     lemmas are first instantiated and then rewrite proceeds. *)
 
-let check_evar_map_of_evars_defs evd =
+let check_evar_map_of_evars_defs env evd =
  let metas = Evd.meta_list evd in
  let check_freemetas_is_empty rebus =
   Evd.Metaset.iter
    (fun m ->
-     if Evd.meta_defined evd m then () else
-      raise
-	(Logic.RefinerError (Logic.UnresolvedBindings [Evd.meta_name evd m])))
+     if Evd.meta_defined evd m then ()
+     else begin
+       raise
+         (Logic.RefinerError (env, evd, Logic.UnresolvedBindings [Evd.meta_name evd m]))
+     end)
  in
   List.iter
    (fun (_,binding) ->
@@ -2063,7 +2065,7 @@ let unification_rewrite l2r c1 c2 sigma prf car rel but env =
   let c1 = if l2r then nf c' else nf c1
   and c2 = if l2r then nf c2 else nf c'
   and car = nf car and rel = nf rel in
-  check_evar_map_of_evars_defs sigma;
+  check_evar_map_of_evars_defs env sigma;
   let prf = nf prf in
   let prfty = nf (Retyping.get_type_of env sigma prf) in
   let sort = sort_of_rel env sigma but in
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index e0d7eca5f..9e47db1c3 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -420,7 +420,7 @@ let interp_hyp ist env sigma (loc,id as locid) =
   with Not_found ->
   (* Then look if bound in the proof context at calling time *)
   if is_variable env id then id
-  else Loc.raise ?loc (Logic.RefinerError (Logic.NoSuchHyp id))
+  else Loc.raise ?loc (Logic.RefinerError (env, sigma, Logic.NoSuchHyp id))
 
 let interp_hyp_list_as_list ist env sigma (loc,id as x) =
   try coerce_to_hyp_list env sigma (Id.Map.find id ist.lfun)
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index c36630f5d..6d5ee504e 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -322,16 +322,16 @@ let coercion_value { coe_value = c; coe_type = t; coe_context = ctx;
 (* pretty-print functions are now in Pretty *)
 (* rajouter une coercion dans le graphe *)
 
-let path_printer = ref (fun _ -> str "<a class path>"
-                        : (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t)
+let path_printer : (env -> Evd.evar_map -> (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) ref =
+  ref (fun _ _ _ -> str "<a class path>")
 
 let install_path_printer f = path_printer := f
 
-let print_path x = !path_printer x
+let print_path env sigma x = !path_printer env sigma x
 
-let message_ambig l =
-  (str"Ambiguous paths:" ++ spc () ++
-   prlist_with_sep fnl (fun ijp -> print_path ijp) l)
+let message_ambig env sigma l =
+  str"Ambiguous paths:" ++ spc () ++
+  prlist_with_sep fnl (fun ijp -> print_path env sigma ijp) l
 
 (* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit
                          coercion,source,target *)
@@ -344,8 +344,8 @@ let different_class_params i =
       | CL_IND i -> Global.is_polymorphic (IndRef i)
       | CL_CONST c -> Global.is_polymorphic (ConstRef c)
       | _ -> false
-	
-let add_coercion_in_graph (ic,source,target) =
+
+let add_coercion_in_graph env sigma (ic,source,target) =
   let old_inheritance_graph = !inheritance_graph in
   let ambig_paths =
     (ref [] : ((cl_index * cl_index) * inheritance_path) list ref) in
@@ -387,7 +387,7 @@ let add_coercion_in_graph (ic,source,target) =
   end;
   let is_ambig = match !ambig_paths with [] -> false | _ -> true in
   if is_ambig && not !Flags.quiet then
-    Feedback.msg_info (message_ambig !ambig_paths)
+    Feedback.msg_info (message_ambig env sigma !ambig_paths)
 
 type coercion = {
   coercion_type   : coe_typ;
@@ -433,13 +433,13 @@ let _ =
       optread  = (fun () -> !automatically_import_coercions);
       optwrite = (:=) automatically_import_coercions }
 
-let cache_coercion (_, c) =
+let cache_coercion env sigma (_, c) =
   let () = add_class c.coercion_source in
   let () = add_class c.coercion_target in
   let is, _ = class_info c.coercion_source in
   let it, _ = class_info c.coercion_target in
-  let value, ctx = Universes.fresh_global_instance (Global.env()) c.coercion_type in
-  let typ = Retyping.get_type_of (Global.env ()) Evd.empty (EConstr.of_constr value) in
+  let value, ctx = Universes.fresh_global_instance env c.coercion_type in
+  let typ = Retyping.get_type_of env sigma (EConstr.of_constr value) in
   let typ = EConstr.Unsafe.to_constr typ in
   let xf =
     { coe_value = value;
@@ -450,15 +450,15 @@ let cache_coercion (_, c) =
       coe_is_projection = c.coercion_is_proj;
       coe_param = c.coercion_params } in
   let () = add_new_coercion c.coercion_type xf in
-  add_coercion_in_graph (xf,is,it)
+  add_coercion_in_graph env sigma (xf,is,it)
 
 let load_coercion _ o =
   if !automatically_import_coercions then
-    cache_coercion o
+    cache_coercion (Global.env ()) Evd.empty o
 
 let open_coercion i o =
   if Int.equal i 1 && not !automatically_import_coercions then
-    cache_coercion o
+    cache_coercion (Global.env ()) Evd.empty o
 
 let subst_coercion (subst, c) =
   let coe = subst_coe_typ subst c.coercion_type in
@@ -497,7 +497,9 @@ let inCoercion : coercion -> obj =
   declare_object {(default_object "COERCION") with
     open_function = open_coercion;
     load_function = load_coercion;
-    cache_function = cache_coercion;
+    cache_function = (fun objn ->
+        let env = Global.env () in cache_coercion env Evd.empty objn
+      );
     subst_function = subst_coercion;
     classify_function = classify_coercion;
     discharge_function = discharge_coercion }
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index b41d0efac..47b41f17b 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -96,7 +96,7 @@ val lookup_pattern_path_between :
 (**/**)
 (* Crade *)
 val install_path_printer :
-  ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit
+  (env -> evar_map -> (cl_index * cl_index) * inheritance_path -> Pp.t) -> unit
 (**/**)
 
 (** {6 This is for printing purpose } *)
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 1eb2c31c8..647111bbe 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -903,18 +903,16 @@ let print_class i =
   let cl,_ = class_info_from_index i in
   pr_class cl
 
-let print_path ((i,j),p) =
-  let sigma, env = Pfedit.get_current_context () in
+let print_path env sigma ((i,j),p) =
   hov 2 (
     str"[" ++ hov 0 (prlist_with_sep pr_semicolon (print_coercion_value env sigma) p) ++
     str"] : ") ++
   print_class i ++ str" >-> " ++ print_class j
 
-(* XXX: This is suspicious!!! *)
 let _ = Classops.install_path_printer print_path
 
-let print_graph () =
-  prlist_with_sep fnl print_path (inheritance_graph())
+let print_graph env sigma =
+  prlist_with_sep fnl (print_path env sigma) (inheritance_graph())
 
 let print_classes () =
   pr_sequence pr_class (classes())
@@ -929,7 +927,7 @@ let index_of_class cl =
     user_err ~hdr:"index_of_class"
       (pr_class cl ++ spc() ++ str "not a defined class.")
 
-let print_path_between cls clt =
+let print_path_between env sigma cls clt =
   let i = index_of_class cls in
   let j = index_of_class clt in
   let p =
@@ -940,7 +938,7 @@ let print_path_between cls clt =
         (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt
 	 ++ str ".")
   in
-  print_path ((i,j),p)
+  print_path env sigma ((i,j),p)
 
 let print_canonical_projections env sigma =
   prlist_with_sep fnl
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 8f3a6ddc4..fd7f1f92b 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -12,6 +12,7 @@ open Reductionops
 open Libnames
 open Globnames
 open Misctypes
+open Evd
 
 (** A Pretty-Printer for the Calculus of Inductive Constructions. *)
 
@@ -39,10 +40,10 @@ val print_about : env -> Evd.evar_map -> reference or_by_notation ->
 val print_impargs : reference or_by_notation -> Pp.t
 
 (** Pretty-printing functions for classes and coercions *)
-val print_graph : unit -> Pp.t
+val print_graph : env -> evar_map -> Pp.t
 val print_classes : unit -> Pp.t
 val print_coercions : env -> Evd.evar_map -> Pp.t
-val print_path_between : Classops.cl_typ -> Classops.cl_typ -> Pp.t
+val print_path_between : env -> evar_map -> Classops.cl_typ -> Classops.cl_typ -> Pp.t
 val print_canonical_projections : env -> Evd.evar_map -> Pp.t
 
 (** Pretty-printing functions for type classes and instances *)
diff --git a/printing/printer.ml b/printing/printer.ml
index 6a0597860..a63004ceb 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -905,7 +905,7 @@ end
 module ContextObjectSet = Set.Make (OrderedContextObject)
 module ContextObjectMap = Map.Make (OrderedContextObject)
 
-let pr_assumptionset env s =
+let pr_assumptionset env sigma s =
   if ContextObjectMap.is_empty s &&
        engagement env = PredicativeSet then
     str "Closed under the global context"
@@ -921,7 +921,6 @@ let pr_assumptionset env s =
       with e when CErrors.noncritical e -> mt ()
     in
     let safe_pr_ltype_relctx (rctx, typ) =
-      let sigma, env = Pfedit.get_current_context () in
       let env = Environ.push_rel_context rctx env in
       try str " " ++ pr_ltype_env env sigma typ
       with e when CErrors.noncritical e -> mt ()
diff --git a/printing/printer.mli b/printing/printer.mli
index 36ca1bdcc..804014745 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -217,8 +217,7 @@ module ContextObjectSet : Set.S with type elt = context_object
 module ContextObjectMap : CMap.ExtS
   with type key = context_object and module Set := ContextObjectSet
 
-val pr_assumptionset :
-  env -> types ContextObjectMap.t -> Pp.t
+val pr_assumptionset : env -> evar_map -> types ContextObjectMap.t -> Pp.t
 
 val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t
 
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 4a92c3856..8bd5d98cb 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -54,9 +54,10 @@ let clenv_value_cast_meta clenv =
 
 let clenv_pose_dependent_evars with_evars clenv =
   let dep_mvs = clenv_dependent clenv in
+  let env, sigma = clenv.env, clenv.evd in
   if not (List.is_empty dep_mvs) && not with_evars then
     raise
-      (RefinerError (UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs)));
+      (RefinerError (env, sigma, UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs)));
   clenv_pose_metas_as_evars clenv dep_mvs
 
 (** Use our own fast path, more informative than from Typeclasses *)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index a9ad606a0..1d86a0909 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -40,7 +40,7 @@ type refiner_error =
   | DoesNotOccurIn of constr * Id.t
   | NoSuchHyp of Id.t
 
-exception RefinerError of refiner_error
+exception RefinerError of Environ.env * Evd.evar_map * refiner_error
 
 open Pretype_errors
 
@@ -69,7 +69,7 @@ let catchable_exception = function
   | PretypeError(_,_, e) -> is_unification_error e || is_typing_error e 
   | _ -> false
 
-let error_no_such_hypothesis id = raise (RefinerError (NoSuchHyp id))
+let error_no_such_hypothesis env sigma id = raise (RefinerError (env, sigma, NoSuchHyp id))
 
 (* Tells if the refiner should check that the submitted rules do not
    produce invalid subgoals *)
@@ -78,10 +78,10 @@ let with_check = Flags.with_option check
 
 (* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and
    returns [tail::(f head (id,_,_) (rev tail))] *)
-let apply_to_hyp check sign id f =
+let apply_to_hyp env sigma check sign id f =
   try apply_to_hyp sign id f
   with Hyp_not_found ->
-    if check then error_no_such_hypothesis id
+    if check then error_no_such_hypothesis env sigma id
     else sign
 
 let check_typability env sigma c =
@@ -147,7 +147,7 @@ let reorder_context env sigma sign ord =
           step ord' expected ctxt_head mh (d::ctxt_tail)
       | _ ->
           (match ctxt_head with
-            | [] -> error_no_such_hypothesis (List.hd ord)
+            | [] -> error_no_such_hypothesis env sigma (List.hd ord)
             | d :: ctxt ->
                 let x = NamedDecl.get_id d in
                 if Id.Set.mem x expected then
@@ -190,9 +190,9 @@ let move_location_eq m1 m2 = match m1, m2 with
 | MoveFirst, MoveFirst -> true
 | _ -> false
 
-let split_sign hfrom hto l =
+let split_sign env sigma hfrom hto l =
   let rec splitrec left toleft = function
-    | [] -> error_no_such_hypothesis hfrom
+    | [] -> error_no_such_hypothesis env sigma hfrom
     | d :: right ->
         let hyp = NamedDecl.get_id d in
       	if Id.equal hyp hfrom then
@@ -222,7 +222,7 @@ let move_hyp sigma toleft (left,declfrom,right) hto =
   let rec moverec first middle = function
     | [] ->
 	if match hto with MoveFirst | MoveLast -> false | _ -> true then
-	  error_no_such_hypothesis (hyp_of_move_location hto);
+          error_no_such_hypothesis env sigma (hyp_of_move_location hto);
 	List.rev first @ List.rev middle
     | d :: _ as right when move_location_eq hto (MoveBefore (NamedDecl.get_id d)) ->
 	List.rev first @ List.rev middle @ right
@@ -258,10 +258,10 @@ let move_hyp sigma toleft (left,declfrom,right) hto =
     List.fold_left (fun sign d -> push_named_context_val d sign)
       right left
 
-let move_hyp_in_named_context sigma hfrom hto sign =
+let move_hyp_in_named_context env sigma hfrom hto sign =
   let open EConstr in
   let (left,right,declfrom,toleft) =
-    split_sign hfrom hto (named_context_of_val sign) in
+    split_sign env sigma hfrom hto (named_context_of_val sign) in
   move_hyp sigma toleft (left,declfrom,right) hto
 
 let insert_decl_in_named_context sigma decl hto sign =
@@ -293,15 +293,15 @@ let collect_meta_variables c =
   in
   List.rev (collrec false [] c)
 
-let check_meta_variables c =
+let check_meta_variables env sigma c =
   if not (List.distinct_f Int.compare (collect_meta_variables c)) then
-    raise (RefinerError (NonLinearProof c))
+    raise (RefinerError (env, sigma, NonLinearProof c))
 
 let check_conv_leq_goal env sigma arg ty conclty =
   if !check then
     let evm, b = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in
       if b then evm 
-      else raise (RefinerError (BadType (arg,ty,conclty)))
+      else raise (RefinerError (env, sigma, BadType (arg,ty,conclty)))
   else sigma
 
 exception Stop of EConstr.t list
@@ -336,7 +336,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
       | Meta _ ->
 	let conclty = nf_betaiota sigma (EConstr.of_constr conclty) in
 	  if !check && occur_meta sigma conclty then
-	    raise (RefinerError (MetaInType conclty));
+            raise (RefinerError (env, sigma, MetaInType conclty));
 	  let (gl,ev,sigma) = mk_goal hyps conclty in
 	  let ev = EConstr.Unsafe.to_constr ev in
 	  let conclty = EConstr.Unsafe.to_constr conclty in
@@ -477,7 +477,9 @@ and mk_arggoals sigma goal goalacc funty allargs =
     | Prod (_, c1, b) ->
       let (acc, hargty, sigma, arg) = mk_refgoals sigma goal goalacc c1 harg in
       (acc, subst1 harg b, sigma), arg
-    | _ -> raise (RefinerError (CannotApply (t, harg)))
+    | _ ->
+      let env = Goal.V82.env sigma goal in
+      raise (RefinerError (env,sigma,CannotApply (t, harg)))
   in
   Array.smartfoldmap foldmap (goalacc, funty, sigma) allargs
 
@@ -497,10 +499,10 @@ and mk_casegoals sigma goal goalacc p c =
 let convert_hyp check sign sigma d =
   let id = NamedDecl.get_id d in
   let b = NamedDecl.get_value d in
-  let env = Global.env() in
+  let env = Global.env () in
   let reorder = ref [] in
   let sign' =
-    apply_to_hyp check sign id
+    apply_to_hyp env sigma check sign id
       (fun _ d' _ ->
         let c = Option.map EConstr.of_constr (NamedDecl.get_value d') in
         let env = Global.env_of_context sign in
@@ -514,19 +516,18 @@ let convert_hyp check sign sigma d =
        map_named_decl EConstr.Unsafe.to_constr d) in
   reorder_val_context env sigma sign' !reorder
 
-
-
 (************************************************************************)
 (************************************************************************)
 (* Primitive tactics are handled here *)
 
 let prim_refiner r sigma goal =
+  let env = Goal.V82.env sigma goal in
   let cl = Goal.V82.concl sigma goal in
   match r with
     (* Logical rules *)
     | Refine c ->
         let cl = EConstr.Unsafe.to_constr cl in
-	check_meta_variables c;
+        check_meta_variables env sigma c;
 	let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl c in
 	let sgl = List.rev sgl in
 	let sigma = Goal.V82.partial_solution sigma goal (EConstr.of_constr oterm) in
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 7df7fd66b..afd1ecf70 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -50,16 +50,16 @@ type refiner_error =
   | DoesNotOccurIn of constr * Id.t
   | NoSuchHyp of Id.t
 
-exception RefinerError of refiner_error
+exception RefinerError of Environ.env * evar_map * refiner_error
 
-val error_no_such_hypothesis : Id.t -> 'a
+val error_no_such_hypothesis : Environ.env -> evar_map -> Id.t -> 'a
 
 val catchable_exception : exn -> bool
 
 val convert_hyp : bool -> Environ.named_context_val -> evar_map ->
   EConstr.named_declaration -> Environ.named_context_val
 
-val move_hyp_in_named_context : Evd.evar_map -> Id.t -> Id.t Misctypes.move_location ->
+val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t Misctypes.move_location ->
   Environ.named_context_val -> Environ.named_context_val
 
 val insert_decl_in_named_context : Evd.evar_map ->
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index cab8d7b52..d41541251 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -55,10 +55,11 @@ let pf_nth_hyp_id gls n = List.nth (pf_hyps gls) (n-1) |> NamedDecl.get_id
 let pf_last_hyp gl = List.hd (pf_hyps gl)
 
 let pf_get_hyp gls id =
+  let env, sigma = pf_env gls, project gls in
   try
     Context.Named.lookup id (pf_hyps gls)
   with Not_found ->
-    raise (RefinerError (NoSuchHyp id))
+    raise (RefinerError (env, sigma, NoSuchHyp id))
 
 let pf_get_hyp_typ gls id =
   id |> pf_get_hyp gls |> NamedDecl.get_type
@@ -182,9 +183,10 @@ module New = struct
 
   let pf_get_hyp id gl =
     let hyps = Proofview.Goal.env gl in
+    let sigma = project gl in
     let sign =
       try EConstr.lookup_named id hyps
-      with Not_found -> raise (RefinerError (NoSuchHyp id))
+      with Not_found -> raise (RefinerError (hyps, sigma, NoSuchHyp id))
     in
     sign
 
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 =
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
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 63768d9b8..16a212511 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1656,13 +1656,13 @@ let vernac_print ~atts env sigma =
   | PrintMLModules -> msg_notice (Mltop.print_ml_modules ())
   | PrintDebugGC -> msg_notice (Mltop.print_gc ())
   | PrintName (qid,udecl) -> dump_global qid; msg_notice (print_name env sigma qid udecl)
-  | PrintGraph -> msg_notice (Prettyp.print_graph())
+  | PrintGraph -> msg_notice (Prettyp.print_graph env sigma)
   | PrintClasses -> msg_notice (Prettyp.print_classes())
   | PrintTypeClasses -> msg_notice (Prettyp.print_typeclasses())
   | PrintInstances c -> msg_notice (Prettyp.print_instances (smart_global c))
   | PrintCoercions -> msg_notice (Prettyp.print_coercions env sigma)
   | PrintCoercionPaths (cls,clt) ->
-      msg_notice (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt))
+      msg_notice (Prettyp.print_path_between env sigma (cl_of_qualid cls) (cl_of_qualid clt))
   | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections env sigma)
   | PrintUniverses (b, dst) ->
      let univ = Global.universes () in
@@ -1696,7 +1696,7 @@ let vernac_print ~atts env sigma =
       let st = Conv_oracle.get_transp_state (Environ.oracle (Global.env())) in
       let nassums =
 	Assumptions.assumptions st ~add_opaque:o ~add_transparent:t gr cstr in
-      msg_notice (Printer.pr_assumptionset (Global.env ()) nassums)
+      msg_notice (Printer.pr_assumptionset env sigma nassums)
   | PrintStrategy r -> print_strategy r
 
 let global_module r =