WARNING: partial commit.

[helm.git] / matita / components / ng_library / nCicLibrary.ml

diff --git a/matita/components/ng_library/nCicLibrary.ml b/matita/components/ng_library/nCicLibrary.ml
index d4ea77a317ba7be499218c693ed028c62bd8dfae..70be8ae5768c31cf13bdc2c7e75a63dda843cf7c 100644 (file)
--- a/matita/components/ng_library/nCicLibrary.ml
+++ b/matita/components/ng_library/nCicLibrary.ml
@@ -146,19 +146,11 @@ let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps=
 
 let init = load_db;;
 
-class type g_status =
- object
-  method timestamp: timestamp
- end
-
 class status =
  object(self)
   val timestamp = (time0 : timestamp)
   method timestamp = timestamp
   method set_timestamp v = {< timestamp = v >}
-  method set_library_status
-   : 'status. #g_status as 'status -> 'self
-   = fun o -> self#set_timestamp o#timestamp
  end
 
 let time_travel status =