]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/ng_library/nCicLibrary.mli
- LexiconAst merged into GrafiteAst
[helm.git] / matita / components / ng_library / nCicLibrary.mli
index de53755f46b674d6cf4d6601723b1c15a91451bc..b2015a9528f1def60d0f8dc869021dcd9a565520 100644 (file)
 (* $Id$ *)
 
 exception LibraryOutOfSync of string Lazy.t
+exception IncludedFileNotCompiled of string * string 
 
 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 *)