NCicMetaSubst.delift
~unify:(fun m s c t1 t2 ->
try Some (NCicUnification.unify
- status.estatus.NEstatus.rstatus m s c t1 t2)
+ status.estatus.NEstatus.rstatus.NRstatus.refiner_status m s c t1 t2)
with
| NCicUnification.UnificationFailure _
| NCicUnification.Uncertain _ -> None)
let status, (_,_,b) = relocate status ctx b in
let n,h,metasenv,subst,o = status.pstatus in
let metasenv, subst =
- NCicUnification.unify status.estatus.NEstatus.rstatus metasenv subst ctx a b
+ NCicUnification.unify status.estatus.NEstatus.rstatus.NRstatus.refiner_status metasenv subst ctx a b
in
{ status with pstatus = n,h,metasenv,subst,o }
;;
let status, (n,_, e) = relocate status ctx e in status, n, Some e
in
let name,height,metasenv,subst,obj = status.pstatus in
- let rdb = status.estatus.NEstatus.rstatus in
+ let rdb = status.estatus.NEstatus.rstatus.NRstatus.refiner_status in
let metasenv, subst, t, ty =
NCicRefiner.typeof rdb metasenv subst ctx term expty
in