Avoid passing dummy env to error printer

5 files changed, 9 insertions, 9 deletions

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index a284c3bfc7..5d75b28539 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -940,7 +940,7 @@ let pf_saturate ?beta ?bi_types gl c ?ty m =
 
 let pf_partial_solution gl t evl =
   let sigma, g = project gl, sig_it gl in
-  let sigma = Goal.V82.partial_solution sigma g t in
+  let sigma = Goal.V82.partial_solution (pf_env gl) sigma g t in
   re_sig (List.map (fun x -> (fst (EConstr.destEvar sigma x))) evl) sigma
 
 let dependent_apply_error =
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 7f67487f5d..bb6decd848 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -1048,7 +1048,7 @@ let thin id sigma goal =
   | None -> sigma
   | Some (sigma, hyps, concl) ->
     let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl in
-    let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
+    let sigma = Goal.V82.partial_solution_to env sigma goal gl ev in
     sigma
 
 (*
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 4e540de538..7245d4a004 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -72,18 +72,18 @@ module V82 = struct
     (evk, ev, evars)
 
   (* Instantiates a goal with an open term *)
-  let partial_solution sigma evk c =
+  let partial_solution env sigma evk c =
     (* Check that the goal itself does not appear in the refined term *)
     let _ =
       if not (Evarutil.occur_evar_upto sigma evk c) then ()
-      else Pretype_errors.error_occur_check Environ.empty_env sigma evk c
+      else Pretype_errors.error_occur_check env sigma evk c
     in
     Evd.define evk c sigma
 
   (* Instantiates a goal with an open term, using name of goal for evk' *)
-  let partial_solution_to sigma evk evk' c =
+  let partial_solution_to env sigma evk evk' c =
     let id = Evd.evar_ident evk sigma in
-    let sigma = partial_solution sigma evk c in
+    let sigma = partial_solution env sigma evk c in
     match id with
     | None -> sigma
     | Some id -> Evd.rename evk' id sigma
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 3b31cff8d7..af9fb662bf 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -48,11 +48,11 @@ module V82 : sig
                          goal * EConstr.constr * Evd.evar_map
 
   (* Instantiates a goal with an open term *)
-  val partial_solution : Evd.evar_map -> goal -> EConstr.constr -> Evd.evar_map
+  val partial_solution : Environ.env -> Evd.evar_map -> goal -> EConstr.constr -> Evd.evar_map
 
   (* Instantiates a goal with an open term, reusing name of goal for
      second goal *)
-  val partial_solution_to : Evd.evar_map -> goal -> goal -> EConstr.constr -> Evd.evar_map
+  val partial_solution_to : Environ.env -> Evd.evar_map -> goal -> goal -> EConstr.constr -> Evd.evar_map
 
   (* Principal part of the progress tactical *)
   val progress : goal list Evd.sigma -> goal Evd.sigma -> bool
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 254c93d0a2..b8612cd2c0 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -590,5 +590,5 @@ let prim_refiner r sigma goal =
         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
+        let sigma = Goal.V82.partial_solution env sigma goal (EConstr.of_constr oterm) in
 	  (sgl, sigma)