Fixed wrong types in proof terms

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

diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli
index c04df8d37b076750fa5a269cfc2fb467141b4ed7..307154127269847e22ce56570ae6f7f5199027f3 100644 (file)
--- a/helm/software/components/ng_tactics/nTacStatus.mli
+++ b/helm/software/components/ng_tactics/nTacStatus.mli
@@ -16,7 +16,7 @@ val fail: string lazy_t -> 'a
 
 type lowtac_status = {
         pstatus : NCic.obj;
-        lstatus : LexiconEngine.status
+        estatus : NEstatus.status;
 }
 
 type lowtactic = lowtac_status -> int -> lowtac_status