Fixed wrong types in proof terms

[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 6aaf4a4a8243ba96673aa34a3a4c00ad23fb17cf..cffda3b174376ea6921a58540bdb9f6cc4119f7e 100644 (file)
--- 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 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 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 in
+  let rdb = status.estatus in
   let metasenv, subst, t, ty = 
    NCicRefiner.typeof rdb metasenv subst ctx term expty
   in