]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/ng_library/nCicLibrary.mli
WARNING: partial commit.
[helm.git] / matita / components / ng_library / nCicLibrary.mli
index de53755f46b674d6cf4d6601723b1c15a91451bc..bad0d89752eddcaa92658a49cde7ee51614901e7 100644 (file)
@@ -15,16 +15,10 @@ exception LibraryOutOfSync of string Lazy.t
 
 type timestamp
 
-class type g_status =
- object
-  method timestamp: timestamp
- end
-
 class status :
  object ('self)
-  inherit g_status
+  method timestamp: timestamp
   method set_timestamp: timestamp -> 'self
-  method set_library_status: #g_status -> 'self
  end
 
 (* it also checks it and add it to the environment *)