From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 9 Dec 2009 16:10:09 +0000 (+0000)
Subject: Added the paramodulation stuff to the status
X-Git-Tag: make_still_working~3170
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=be163baeff523f00b6ac865bb4af700b0a51d288;p=helm.git

Added the paramodulation stuff to the status
---

diff --git a/helm/software/components/ng_library/nCicLibrary.ml b/helm/software/components/ng_library/nCicLibrary.ml
index c5b43d7ca..7cef1e3de 100644
--- a/helm/software/components/ng_library/nCicLibrary.ml
+++ b/helm/software/components/ng_library/nCicLibrary.ml
@@ -144,10 +144,26 @@ 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 =
@@ -210,6 +226,7 @@ class type g_dumpable_status =
  object
   inherit g_status
   inherit g_auto_status
+  inherit g_eq_status
   method dump: obj list
  end
 
@@ -217,11 +234,13 @@ 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
+   = fun o -> 
+     (((self#set_dump o#dump)#set_coercion_status o)#set_auto_status o)#set_eq_status o
  end
 
 type 'a register_type =
diff --git a/helm/software/components/ng_library/nCicLibrary.mli b/helm/software/components/ng_library/nCicLibrary.mli
index ea1cfd4e5..03b844397 100644
--- a/helm/software/components/ng_library/nCicLibrary.mli
+++ b/helm/software/components/ng_library/nCicLibrary.mli
@@ -14,6 +14,19 @@
 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
@@ -64,6 +77,7 @@ class type g_dumpable_status =
  object
   inherit g_status
   inherit g_auto_status
+  inherit g_eq_status
   method dump: obj list
  end
   
@@ -71,6 +85,7 @@ 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