Bad variable name fixed.

[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 729f6ba6eec5e65f93ac85837d388193c9ac9368..631e629e5a663060a1f314fdd738ff809cc90ad9 100644 (file)
--- a/helm/software/components/ng_refiner/nRstatus.mli
+++ b/helm/software/components/ng_refiner/nRstatus.mli
@@ -11,15 +11,7 @@
 
 (* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *)
 
-type refiner_status = {
-        coerc_db : NCicCoercion.db;
-        uhint_db : NCicUnifHint.db;
-        library_db : NCicLibrary.timestamp;
-}
+class type g_status = NCicCoercion.status
 
-module Serializer: NCicLibrary.Serializer with type status = refiner_status
+class status : NCicCoercion.status
 
-type dumpable_refiner_status = {
-        refiner_status : refiner_status;
-        dump: Serializer.obj list
-}