Changed auto from implicit to option and renamed a few functions.

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

diff --git a/components/tactics/paramodulation/saturation.mli b/components/tactics/paramodulation/saturation.mli
index d16c9e28a8aa9f8653b149c82b8c03fd025f5e5c..aa8f24ec3f0a842b011d95ba6fc14634ba13a791 100644 (file)
--- a/components/tactics/paramodulation/saturation.mli
+++ b/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:Equality_retrieval.auto_type ->
+  Equality_retrieval.auto_type option ->
   ProofEngineTypes.status ->
   ProofEngineTypes.proof * ProofEngineTypes.goal list
 
@@ -46,17 +46,18 @@ val find_equalities:
   HMysql.dbd ->
   ProofEngineTypes.status ->
   bool -> (* smart_flag *)
-  ?auto:Equality_retrieval.auto_type -> 
-  AutoCache.cache ->
+  Equality_retrieval.auto_type option -> 
+  AutoCache.cache -> 
   Equality.equality_bag *
     Equality.equality list * AutoCache.cache * int
-val saturate_more: 
+
+val close_more: 
   Equality.equality_bag ->
   active_table ->
   int -> (* maxmeta *)
   ProofEngineTypes.status ->
   bool -> (* smart flag *)
-  ?auto:Equality_retrieval.auto_type ->
+  Equality_retrieval.auto_type option ->
   AutoCache.cache ->
     Equality.equality_bag * Equality.equality list * AutoCache.cache * int