From 6839a2c9b7d2480e21572a7d176dcd6ea0617159 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 30 Apr 2020 16:05:19 +0200
Subject: Remove a very specific low-level tactical from Refiner.

It was only used at one point in the STM, and its localization was suprising
to say the least. Furthermore it was relying on legacy code. Instead we hardcode
it in the STM.
---
 stm/stm.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index f3768e9b99..5790bfc07e 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2023,12 +2023,16 @@ end = struct (* {{{ *)
           match Future.join f with
           | Some (pt, uc) ->
             let sigma, env = PG_compat.get_current_context () in
+            let push_state ctx =
+              Proofview.tclEVARMAP >>= fun sigma ->
+              Proofview.Unsafe.tclEVARS (Evd.merge_universe_context sigma ctx)
+            in
             stm_pperr_endline (fun () -> hov 0 (
               str"g=" ++ int (Evar.repr gid) ++ spc () ++
               str"t=" ++ (Printer.pr_constr_env env sigma pt) ++ spc () ++
               str"uc=" ++ Termops.pr_evar_universe_context uc));
             (if abstract then Abstract.tclABSTRACT None else (fun x -> x))
-              (V82.tactic (Refiner.tclPUSHEVARUNIVCONTEXT uc) <*>
+              (push_state uc <*>
               Tactics.exact_no_check (EConstr.of_constr pt))
           | None ->
             if solve then Tacticals.New.tclSOLVE [] else tclUNIT ()
-- 
cgit v1.2.3