X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_library%2FnCicLibrary.ml;h=c5b43d7ca52eeb8b3f43db6bb5835c1d01949bbb;hb=a90c31c1b53222bd6d57360c5ba5c2d0fe7d5207;hp=7cef1e3de66fb2ad68ad2684b973527f878cb06b;hpb=4377e950998c9c63937582952a79975947aa9a45;p=helm.git

diff --git a/helm/software/components/ng_library/nCicLibrary.ml b/helm/software/components/ng_library/nCicLibrary.ml
index 7cef1e3de..c5b43d7ca 100644
--- a/helm/software/components/ng_library/nCicLibrary.ml
+++ b/helm/software/components/ng_library/nCicLibrary.ml
@@ -144,26 +144,10 @@ let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps=
 let init = load_db;;
 
 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)
-  val eq_cache = NCicParamod.empty_state
-  method eq_cache = eq_cache
-  method set_eq_cache v = {< eq_cache = v >}
-  method set_eq_status
-   : 'status. #g_eq_status as 'status -> 'self
-   = fun o -> self#set_eq_cache o#eq_cache
- end
 
 class type g_auto_status =
  object
-   method auto_cache : automation_cache
+  method auto_cache : automation_cache
  end
 
 class auto_status =
@@ -226,7 +210,6 @@ class type g_dumpable_status =
  object
   inherit g_status
   inherit g_auto_status
-  inherit g_eq_status
   method dump: obj list
  end
 
@@ -234,13 +217,11 @@ class dumpable_status =
  object(self)
   inherit status
   inherit auto_status
-  inherit eq_status
   val dump = ([] : obj list)
   method dump = dump
   method set_dump v = {< dump = v >}
   method set_dumpable_status : 'status. #g_dumpable_status as 'status -> 'self
-   = fun o -> 
-     (((self#set_dump o#dump)#set_coercion_status o)#set_auto_status o)#set_eq_status o
+   = fun o -> ((self#set_dump o#dump)#set_coercion_status o)#set_auto_status o
  end
 
 type 'a register_type =