Remove legacy API in SSR.

3 files changed, 9 insertions, 9 deletions

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 238b94ae49..1cc879559d 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -902,7 +902,7 @@ let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, CastConv ty)
 let rec isCHoles = function { CAst.v = CHole _ } :: cl -> isCHoles cl | cl -> cl = []
 let rec isCxHoles = function ({ CAst.v = CHole _ }, None) :: ch -> isCxHoles ch | _ -> false
 
-let pf_interp_ty ?(resolve_typeclasses=false) ist gl ty =
+let pf_interp_ty ?(resolve_typeclasses=false) env sigma0 ist ty =
    let n_binders = ref 0 in
    let ty = match ty with
    | a, (t, None) ->
@@ -927,15 +927,14 @@ let pf_interp_ty ?(resolve_typeclasses=false) ist gl ty =
      | LetInType(n,v,ty,t) -> decr n_binders; mkLetIn (n, v, ty, aux t)
      | _ -> anomaly "pf_interp_ty: ssr Type cast deleted by typecheck" in
      sigma, aux t in
-   let sigma, cty as ty = strip_cast (interp_term (pf_env gl) (project gl) ist ty) in
+   let sigma, cty as ty = strip_cast (interp_term env sigma0 ist ty) in
    let ty =
-     let env = pf_env gl in
      if not resolve_typeclasses then ty
      else
        let sigma = Typeclasses.resolve_typeclasses ~fail:false env sigma in
        sigma, Evarutil.nf_evar sigma cty in
-   let n, c, _, ucst = pf_abs_evars gl ty in
-   let lam_c = pf_abs_cterm gl n c in
+   let n, c, _, ucst = abs_evars env sigma0 ty in
+   let lam_c = abs_cterm env sigma0 n c in
    let ctx, c = EConstr.decompose_lam_n_assum sigma n lam_c in
    n, EConstr.it_mkProd_or_LetIn c ctx, lam_c, ucst
 ;;
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index b82478a23a..e1d6061178 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -320,8 +320,9 @@ val pf_abs_ssrterm :
 
 val pf_interp_ty :
            ?resolve_typeclasses:bool ->
+           Environ.env ->
+           Evd.evar_map ->
            Tacinterp.interp_sign ->
-           Goal.goal Evd.sigma ->
            Ssrast.ssrtermkind *
            (Glob_term.glob_constr * Constrexpr.constr_expr option) ->
            int * EConstr.t * EConstr.t * UState.t
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 6ff59f21a3..d319eba8aa 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -152,7 +152,7 @@ let havetac ist
   let mkl t = (xNoFlag, (t, None)) in
   let interp gl rtc t = pf_abs_ssrterm ~resolve_typeclasses:rtc ist gl t in
   let interp_ty gl rtc t =
-    let a,b,_,u = pf_interp_ty ~resolve_typeclasses:rtc ist gl t in a,b,u in
+    let a,b,_,u = pf_interp_ty ~resolve_typeclasses:rtc (pf_env gl) (project gl) ist t in a,b,u in
   let open CAst in
   let ct, cty, hole, loc = match Ssrcommon.ssrterm_of_ast_closure_term t with
     | _, (_, Some { loc; v = CCast (ct, CastConv cty)}) ->
@@ -261,7 +261,7 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave =
     let (sigma, ev) = Evarutil.new_evar env sigma EConstr.mkProp in
     let k, _ = EConstr.destEvar sigma ev in
     let fake_gl = {Evd.it = k; Evd.sigma = sigma} in
-    let _, ct, _, uc = pf_interp_ty ist fake_gl ct in
+    let _, ct, _, uc = pf_interp_ty (pf_env fake_gl) sigma ist ct in
     let rec var2rel c g s = match EConstr.kind sigma c, g with
       | Prod({binder_name=Anonymous} as x,_,c), [] -> EConstr.mkProd(x, EConstr.Vars.subst_vars s ct, c)
       | Sort _, [] -> EConstr.Vars.subst_vars s ct
@@ -335,7 +335,7 @@ let sufftac ist ((((clr, pats),binders),simpl), ((_, c), hint)) =
   in
   let ctac =
     Proofview.V82.tactic begin fun gl ->
-    let _,ty,_,uc = pf_interp_ty ist gl c in let gl = pf_merge_uc uc gl in
+    let _,ty,_,uc = pf_interp_ty (pf_env gl) (project gl) ist c in let gl = pf_merge_uc uc gl in
     Proofview.V82.of_tactic (basecuttac "ssr_suff" ty) gl
   end in
   Tacticals.New.tclTHENS ctac [htac; Tacticals.New.tclTHEN (cleartac clr) (introstac (binders@simpl))]