Initial implementation of statuses using objects in place of nested records.

[helm.git] / helm / software / components / ng_tactics / nTacStatus.ml

diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml
index ba030806827beab9fd2c7f21b4ecb762139444d8..6aaf4a4a8243ba96673aa34a3a4c00ad23fb17cf 100644 (file)
--- a/helm/software/components/ng_tactics/nTacStatus.ml
+++ b/helm/software/components/ng_tactics/nTacStatus.ml
@@ -84,7 +84,7 @@ let relocate status destination (name,source,t as orig) =
     NCicMetaSubst.delift 
        ~unify:(fun m s c t1 t2 -> 
          try Some (NCicUnification.unify 
-           status.estatus.NEstatus.rstatus.NRstatus.refiner_status m s c t1 t2)
+           status.estatus.NEstatus.rstatus m s c t1 t2)
          with 
           | NCicUnification.UnificationFailure _ 
           | NCicUnification.Uncertain _ -> None) 
@@ -147,7 +147,7 @@ let unify status ctx a b =
   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.NRstatus.refiner_status metasenv subst ctx a b
+    NCicUnification.unify status.estatus.NEstatus.rstatus metasenv subst ctx a b
   in
   { status with pstatus = n,h,metasenv,subst,o }
 ;;
@@ -160,7 +160,7 @@ let refine status ctx term expty =
         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.NRstatus.refiner_status in
+  let rdb = status.estatus.NEstatus.rstatus in
   let metasenv, subst, t, ty = 
    NCicRefiner.typeof rdb metasenv subst ctx term expty
   in