new version of auto that is able to prove the irrationality of sqrt(2)

[helm.git] / helm / software / components / tactics / paramodulation / saturation.mli

diff --git a/helm/software/components/tactics/paramodulation/saturation.mli b/helm/software/components/tactics/paramodulation/saturation.mli
index 3bd04454c2e5ad2d25817b4775bd9d05c4645578..d16c9e28a8aa9f8653b149c82b8c03fd025f5e5c 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.mli
+++ b/helm/software/components/tactics/paramodulation/saturation.mli
@@ -32,7 +32,7 @@ val saturate : (* FIXME: should be exported a a tactic *)
   ?depth:int ->
   ?width:int ->
   ?timeout:float ->
-  ?auto:Inference.auto_type ->
+  ?auto:Equality_retrieval.auto_type ->
   ProofEngineTypes.status ->
   ProofEngineTypes.proof * ProofEngineTypes.goal list
 
@@ -46,19 +46,19 @@ val find_equalities:
   HMysql.dbd ->
   ProofEngineTypes.status ->
   bool -> (* smart_flag *)
-  ?auto:Inference.auto_type -> 
-  AutoTypes.cache ->
+  ?auto:Equality_retrieval.auto_type -> 
+  AutoCache.cache ->
   Equality.equality_bag *
-    Equality.equality list * AutoTypes.cache * int
+    Equality.equality list * AutoCache.cache * int
 val saturate_more: 
   Equality.equality_bag ->
   active_table ->
   int -> (* maxmeta *)
   ProofEngineTypes.status ->
   bool -> (* smart flag *)
-  ?auto:Inference.auto_type ->
-  AutoTypes.cache ->
-    Equality.equality_bag * Equality.equality list * AutoTypes.cache * int
+  ?auto:Equality_retrieval.auto_type ->
+  AutoCache.cache ->
+    Equality.equality_bag * Equality.equality list * AutoCache.cache * int
 
 val given_clause: 
   Equality.equality_bag ->