X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_library%2FnCicLibrary.mli;h=63bd7518aa538421c45131e0adee55ba9fc8a82c;hb=2a33a51a4749ca91dfaa488b9c0d2a286265cf99;hp=14a0685b4a6a74633a13e8abc7cb093e89fc8887;hpb=75f910c7001ba5a6abe61fc93a2731753c7ba188;p=helm.git diff --git a/matita/components/ng_library/nCicLibrary.mli b/matita/components/ng_library/nCicLibrary.mli index 14a0685b4..63bd7518a 100644 --- a/matita/components/ng_library/nCicLibrary.mli +++ b/matita/components/ng_library/nCicLibrary.mli @@ -16,8 +16,9 @@ exception IncludedFileNotCompiled of string * string type timestamp -class status : +class virtual status : object ('self) + inherit NCic.status method timestamp: timestamp method set_timestamp: timestamp -> 'self end @@ -29,7 +30,7 @@ val add_constraint: val aliases_of: NUri.uri -> NReference.reference list val resolve: string -> NReference.reference list (* warning: get_obj may raise (NCicEnvironment.ObjectNotFoud l) *) -val get_obj: NUri.uri -> NCic.obj (* changes the current timestamp *) +val get_obj: #NCic.status -> NUri.uri -> NCic.obj (* changes the current timestamp *) val time_travel: #status -> unit @@ -50,7 +51,7 @@ class dumpable_status : method set_dumpable_status: #g_dumpable_status -> 'self end -val get_already_included: #dumpable_status -> NUri.uri list +val get_transitively_included: #dumpable_status -> NUri.uri list val dump_obj: #dumpable_status as 'status -> obj -> 'status module type SerializerType = @@ -60,7 +61,7 @@ module type SerializerType = type 'a register_type = 'a -> refresh_uri_in_universe:(NCic.universe -> NCic.universe) -> - refresh_uri_in_term:(NCic.term -> NCic.term) -> + refresh_uri_in_term:(NCic.status -> NCic.term -> NCic.term) -> refresh_uri_in_reference:(NReference.reference -> NReference.reference) -> alias_only:bool -> dumpable_status -> dumpable_status