type lowtac_status = {
pstatus : NCic.obj;
- lstatus : LexiconEngine.status
+ estatus : NEstatus.extra_status;
}
type lowtactic = lowtac_status -> int -> lowtac_status
(List.rev destination, List.rev source)
in
let lc = (0,NCic.Ctx (List.rev lc)) in
- let db = NCicUnifHint.db () in (* XXX fixme *)
let (metasenv, subst), t =
NCicMetaSubst.delift
~unify:(fun m s c t1 t2 ->
- try Some (NCicUnification.unify db m s c t1 t2)
+ try Some (NCicUnification.unify
+ status.estatus.NEstatus.rstatus.NRstatus.refiner_status m s c t1 t2)
with
| NCicUnification.UnificationFailure _
| NCicUnification.Uncertain _ -> None)
let status, (_,_,x) = relocate status context ty in status, Some x
in
let uri,height,metasenv,subst,obj = status.pstatus in
- let metasenv, subst, lexicon_status, t =
+ let metasenv, subst, estatus, t =
GrafiteDisambiguate.disambiguate_nterm expty
- status.lstatus context metasenv subst t
+ status.estatus context metasenv subst t
in
let new_pstatus = uri,height,metasenv,subst,obj in
- { lstatus = lexicon_status; pstatus = new_pstatus }, (None, context, t)
+ { estatus = estatus; pstatus = new_pstatus }, (None, context, t)
;;
let typeof status ctx t =
let status, (_,_,b) = relocate status ctx b in
let n,h,metasenv,subst,o = status.pstatus in
let metasenv, subst =
- NCicUnification.unify (NCicUnifHint.db ()) 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 db = NCicUnifHint.db () in (* XXX fixme *)
- let coercion_db = NCicCoercion.db () in
- let look_for_coercion = NCicCoercion.look_for_coercion coercion_db in
+ let rdb = status.estatus.NEstatus.rstatus.NRstatus.refiner_status in
let metasenv, subst, t, ty =
- NCicRefiner.typeof db ~look_for_coercion metasenv subst ctx term expty
+ NCicRefiner.typeof rdb metasenv subst ctx term expty
in
{ status with pstatus = name,height,metasenv,subst,obj },
(nt,ctx,t), (ne,ctx,ty)