Further port of the SSR tactics.

1 files changed, 6 insertions, 3 deletions

diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 551c316e79..4148102f61 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -393,10 +393,13 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
           let erefl_ty = Retyping.get_type_of (pf_env gl) (project gl) erefl in
           let eq_ty = Retyping.get_type_of (pf_env gl) (project gl) erefl_ty in
           let gen_eq_tac =
-            Proofview.V82.tactic ~nf_evars:false begin fun s ->
+            let open Proofview.Notations in
+            Proofview.Goal.enter begin fun s ->
+            let sigma = Proofview.Goal.sigma s in
             let open Evd in
-            let sigma = merge_universe_context s.sigma (evar_universe_context (project gl)) in
-            apply_type new_concl [erefl] { s with sigma }
+            let sigma = merge_universe_context sigma (evar_universe_context (project gl)) in
+            Proofview.Unsafe.tclEVARS sigma <*>
+            Tactics.apply_type ~typecheck:true new_concl [erefl]
             end
           in
           gen_eq_tac, eq_ty, gl in