type lowtac_status = {
pstatus : NCic.obj;
- estatus : NEstatus.extra_status;
+ estatus : NEstatus.status;
}
type lowtactic = lowtac_status -> int -> lowtac_status
let (metasenv, subst), t =
NCicMetaSubst.delift
~unify:(fun m s c t1 t2 ->
- try Some (NCicUnification.unify
- status.estatus.NEstatus.rstatus m s c t1 t2)
+ try Some (NCicUnification.unify status.estatus 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 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 in
let metasenv, subst, t, ty =
NCicRefiner.typeof rdb metasenv subst ctx term expty
in