X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnRstatus.mli;h=522d7e901b396d373db8b98674ba5eae9f690954;hb=df1201e37d6f2631dc31ffc87b979a6c81180a3a;hp=46634a6799785e7e81b8df74b8cdc7722ccaccd4;hpb=dcdbb979433a61e2ef2842d96604098728824416;p=helm.git diff --git a/helm/software/components/ng_refiner/nRstatus.mli b/helm/software/components/ng_refiner/nRstatus.mli index 46634a679..522d7e901 100644 --- a/helm/software/components/ng_refiner/nRstatus.mli +++ b/helm/software/components/ng_refiner/nRstatus.mli @@ -11,7 +11,22 @@ (* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *) -type refiner_status = { - coerc_db : NCicCoercion.db; - uhint_db : NCicUnifHint.db; -} +class status : + object + inherit NCicUnifHint.status + inherit NCicCoercion.status + inherit NCicLibrary.status + end + +module Serializer: + sig + include NCicLibrary.Serializer with type status = status + val require: baseuri:NUri.uri -> (#status as 'status) -> 'status + end + +class dumpable_status : + object ('self) + inherit status + method dump: Serializer.obj list + method set_dump: Serializer.obj list -> 'self + end