EXPERIMENTAL COMMIT (by CSC,actuall :-)

[helm.git] / helm / software / components / ng_refiner / nRstatus.mli

diff --git a/helm/software/components/ng_refiner/nRstatus.mli b/helm/software/components/ng_refiner/nRstatus.mli
index 46634a6799785e7e81b8df74b8cdc7722ccaccd4..6cf9ddd4fa9c136b77ff8c4cc14b771e55a06880 100644 (file)
--- a/helm/software/components/ng_refiner/nRstatus.mli
+++ b/helm/software/components/ng_refiner/nRstatus.mli
@@ -14,4 +14,6 @@
 type refiner_status = {
         coerc_db : NCicCoercion.db;
         uhint_db : NCicUnifHint.db;
+        library_db : NCicLibrary.timestamp;
+        dump: refiner_status -> refiner_status
 }