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

diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml
index 6aaf4a4a8..ba0308068 100644
--- 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 m s c t1 t2)
+           status.estatus.NEstatus.rstatus.NRstatus.refiner_status 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 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 }
 ;;
@@ -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 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