FIX OF THE PREVIOUS EXPERIMENTAL COMMIT:

[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 0ef8755f4b0fa756f0a7a5e544f3c3b2b2013aaf..26ef2684c11a0a5ebb1f3815e5e0abf5e2c2187f 100644 (file)
--- a/helm/software/components/ng_refiner/nRstatus.ml
+++ b/helm/software/components/ng_refiner/nRstatus.ml
@@ -15,6 +15,12 @@ type refiner_status = {
         coerc_db : NCicCoercion.db;
         uhint_db : NCicUnifHint.db;
         library_db : NCicLibrary.timestamp;
-        dump: refiner_status -> refiner_status
 }
 
+module Serializer =
+ NCicLibrary.Serializer(struct type status = refiner_status end)
+
+type dumpable_refiner_status = {
+        refiner_status : refiner_status;
+        dump: Serializer.obj list
+}