2 files changed, 18 insertions, 16 deletions
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 17a7121a3f..f867a47c08 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -14,10 +14,7 @@ open Constr
 open Context
 open CErrors
 open Evar_refiner
-open Tacmach
 open Tacexpr
-open Refiner
-open Evd
 open Locus
 open Context.Named.Declaration
 open Ltac_pretype
@@ -26,7 +23,11 @@ module NamedDecl = Context.Named.Declaration
 
 (* The instantiate tactic *)
 
-let instantiate_evar evk (ist,rawc) env sigma =
+let instantiate_evar evk (ist,rawc) =
+  let open Proofview.Notations in
+  Proofview.tclENV >>= fun env ->
+  Proofview.Goal.enter begin fun gl ->
+  let sigma = Proofview.Goal.sigma gl in
   let evi = Evd.find sigma evk in
   let filtered = Evd.evar_filtered_env env evi in
   let constrvars = Tacinterp.extract_ltac_constr_values ist filtered in
@@ -37,7 +38,8 @@ let instantiate_evar evk (ist,rawc) env sigma =
     ltac_genargs = ist.Geninterp.lfun;
   } in
   let sigma' = w_refine (evk,evi) (lvar ,rawc) env sigma in
-  tclEVARS sigma'
+  Proofview.Unsafe.tclEVARS sigma'
+  end
 
 let evar_list sigma c =
   let rec evrec acc c =
@@ -47,14 +49,15 @@ let evar_list sigma c =
   evrec [] c
 
 let instantiate_tac n c ido =
-  Proofview.V82.tactic begin fun gl ->
-  let env = Global.env () in
-  let sigma = gl.sigma in
+  Proofview.Goal.enter begin fun gl ->
+  let sigma = Proofview.Goal.sigma gl in
+  let env = Proofview.Goal.env gl in
+  let concl = Proofview.Goal.concl gl in
   let evl =
     match ido with
-        ConclLocation () -> evar_list sigma (pf_concl gl)
+        ConclLocation () -> evar_list sigma concl
       | HypLocation (id,hloc) ->
-          let decl = Environ.lookup_named id (pf_env gl) in
+          let decl = Environ.lookup_named id env in
             match hloc with
                 InHyp ->
                   (match decl with
@@ -70,17 +73,16 @@ let instantiate_tac n c ido =
     user_err Pp.(str "Not enough uninstantiated existential variables.");
   if n <= 0 then user_err Pp.(str "Incorrect existential variable index.");
   let evk,_ = List.nth evl (n-1) in
-  instantiate_evar evk c env sigma gl
+  instantiate_evar evk c
   end
 
 let instantiate_tac_by_name id c =
-  Proofview.V82.tactic begin fun gl ->
-  let env = Global.env () in
-  let sigma = gl.sigma in
+  Proofview.Goal.enter begin fun gl ->
+  let sigma = Proofview.Goal.sigma gl in
   let evk =
     try Evd.evar_key id sigma
     with Not_found -> user_err Pp.(str "Unknown existential variable.") in
-  instantiate_evar evk c env sigma gl
+  instantiate_evar evk c
   end
 
 let let_evar name typ =
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index d1f031b418..5ae0b2efd7 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1087,7 +1087,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
   | TacShowHyps tac ->
          Proofview.V82.tactic begin
            tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac))
-         end
+         end [@ocaml.warning "-3"]
   | TacAbstract (t,ido) ->
       let call = LtacMLCall tac in
       let trace = push_trace(None,call) ist in