diff options
| author | Pierre-Marie Pédrot | 2020-05-01 16:38:21 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-03 13:09:50 +0200 |
| commit | ea11e308be5f7410ea0f032736eb6ec2e686abbe (patch) | |
| tree | b5249a09ace033e1f19c6d2665e2563c169dee3a /plugins/ssr/ssrcommon.ml | |
| parent | 2d00c8b07957206040dbc71598439a601eef4161 (diff) | |
Remove legacy API in SSR.
Diffstat (limited to 'plugins/ssr/ssrcommon.ml')
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 9 |
1 files changed, 4 insertions, 5 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 ;; |