X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTacStatus.ml;h=cffda3b174376ea6921a58540bdb9f6cc4119f7e;hb=c091ca7a030a85a529543de98e45c54284028b63;hp=ba030806827beab9fd2c7f21b4ecb762139444d8;hpb=f6c887944d48d718f372a57f1609f3d059908aa8;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml
index ba0308068..cffda3b17 100644
--- a/helm/software/components/ng_tactics/nTacStatus.ml
+++ b/helm/software/components/ng_tactics/nTacStatus.ml
@@ -16,7 +16,7 @@ let fail msg = raise (Error msg)
 
 type lowtac_status = {
         pstatus : NCic.obj;
-        estatus : NEstatus.extra_status;
+        estatus : NEstatus.status;
 }
 
 type lowtactic = lowtac_status -> int -> lowtac_status 
@@ -83,8 +83,7 @@ let relocate status destination (name,source,t as orig) =
   let (metasenv, subst), t =
     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)
+         try Some (NCicUnification.unify status.estatus m s c t1 t2)
          with 
           | NCicUnification.UnificationFailure _ 
           | NCicUnification.Uncertain _ -> None) 
@@ -147,7 +146,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 metasenv subst ctx a b
   in
   { status with pstatus = n,h,metasenv,subst,o }
 ;;
@@ -160,7 +159,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 in
   let metasenv, subst, t, ty = 
    NCicRefiner.typeof rdb metasenv subst ctx term expty
   in