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

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

diff --git a/components/tactics/paramodulation/equality_retrieval.mli b/components/tactics/paramodulation/equality_retrieval.mli
index e9506580dc2792dc9ab709f894487f687cbe9aa5..7a24e3a556ee0142fbc6abfe478a666e191d94b4 100644 (file)
--- a/components/tactics/paramodulation/equality_retrieval.mli
+++ b/components/tactics/paramodulation/equality_retrieval.mli
@@ -43,7 +43,7 @@ type auto_type =
 val find_context_equalities:
   int -> (* maxmeta *)
   Equality.equality_bag ->
-  ?auto:auto_type ->
+  auto_type option ->
   Cic.context -> ProofEngineTypes.proof -> (* FIXME:Why bot context and proof?*)
   AutoCache.cache -> 
     int list * Equality.equality list * int * AutoCache.cache
@@ -53,7 +53,7 @@ val find_context_equalities:
 *)
 val find_library_equalities:
   Equality.equality_bag ->
-  ?auto:auto_type ->
+  auto_type option->
   bool -> HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int ->
   AutoCache.cache ->  
     UriManager.UriSet.t * (UriManager.uri * Equality.equality) list * int *