]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_library/nCicLibrary.mli
Release 0.5.9.
[helm.git] / helm / software / components / ng_library / nCicLibrary.mli
index 03b84439711b872d317aa295c04fd6880f7570f6..ea1cfd4e523cc008de445256b1c9866156d20128 100644 (file)
 exception LibraryOutOfSync of string Lazy.t
 
 type automation_cache = NDiscriminationTree.DiscriminationTree.t
-type unit_eq_cache = NCicParamod.state
-
-class type g_eq_status =
- object
-   method eq_cache : unit_eq_cache 
- end
-
-class eq_status :
- object('self)
-  inherit g_eq_status
-  method set_eq_cache: unit_eq_cache -> 'self
-  method set_eq_status: #g_eq_status -> 'self
- end
 
 class type g_auto_status =
  object
@@ -77,7 +64,6 @@ class type g_dumpable_status =
  object
   inherit g_status
   inherit g_auto_status
-  inherit g_eq_status
   method dump: obj list
  end
   
@@ -85,7 +71,6 @@ class dumpable_status :
  object ('self)
   inherit status
   inherit auto_status
-  inherit eq_status
   inherit g_dumpable_status
   method set_dump: obj list -> 'self
   method set_dumpable_status: #g_dumpable_status -> 'self