EXPERIMENTAL COMMIT (by CSC,actuall :-)

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

diff --git a/helm/software/components/ng_refiner/nRstatus.ml b/helm/software/components/ng_refiner/nRstatus.ml
index 02eee9837723853c3d616673da31924977b2cc1f..0ef8755f4b0fa756f0a7a5e544f3c3b2b2013aaf 100644 (file)
--- a/helm/software/components/ng_refiner/nRstatus.ml
+++ b/helm/software/components/ng_refiner/nRstatus.ml
@@ -14,5 +14,7 @@
 type refiner_status = {
         coerc_db : NCicCoercion.db;
         uhint_db : NCicUnifHint.db;
+        library_db : NCicLibrary.timestamp;
+        dump: refiner_status -> refiner_status
 }