diff options
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 9 | ||||
| -rw-r--r-- | plugins/ssr/ssrcommon.mli | 3 | ||||
| -rw-r--r-- | plugins/ssr/ssrfwd.ml | 6 |
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))] |