first proof reconstruction attempt, still bugged since it

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