FIX OF THE PREVIOUS EXPERIMENTAL COMMIT:

[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 6cf9ddd4fa9c136b77ff8c4cc14b771e55a06880..729f6ba6eec5e65f93ac85837d388193c9ac9368 100644 (file)
--- a/helm/software/components/ng_refiner/nRstatus.mli
+++ b/helm/software/components/ng_refiner/nRstatus.mli
@@ -15,5 +15,11 @@ type refiner_status = {
         coerc_db : NCicCoercion.db;
         uhint_db : NCicUnifHint.db;
         library_db : NCicLibrary.timestamp;
-        dump: refiner_status -> refiner_status
+}
+
+module Serializer: NCicLibrary.Serializer with type status = refiner_status
+
+type dumpable_refiner_status = {
+        refiner_status : refiner_status;
+        dump: Serializer.obj list
 }