X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnRstatus.mli;h=729f6ba6eec5e65f93ac85837d388193c9ac9368;hb=8de1a75899a83dd31e856804bd448c1bd87d9ab3;hp=6cf9ddd4fa9c136b77ff8c4cc14b771e55a06880;hpb=5c8de084e314e41f3dc2f605f6242283e930b803;p=helm.git

diff --git a/helm/software/components/ng_refiner/nRstatus.mli b/helm/software/components/ng_refiner/nRstatus.mli
index 6cf9ddd4f..729f6ba6e 100644
--- 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
 }