X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.mli;h=efb4e843c99a2e91da86a04144f657c666370c55;hb=60c92de1ace192d20b818bd71ec420d74e0176d2;hp=4af0c3fb7a0d14f01672ad7d6a20c91e3fe7f124;hpb=00da35cbf619e0d1f3d7fde7e6a0e6e4dc6c0915;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli
index 4af0c3fb7..efb4e843c 100644
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -74,6 +74,7 @@ val atomic_tac :
       [> `NoTag ])
      list NTacStatus.status ->
      (< auto_cache : NCicLibrary.automation_cache;
+        eq_cache : NCicLibrary.unit_eq_cache;
         coerc_db : NCicCoercion.db; dump : NCicLibrary.obj list;
         lstatus : LexiconEngine.lexicon_status; obj : NCic.obj;
         set_coerc_db : NCicCoercion.db -> 'c;