X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fequality_retrieval.mli;h=7a24e3a556ee0142fbc6abfe478a666e191d94b4;hb=1f829cda7957b48cac8109a3721ded11f6cec8de;hp=e9506580dc2792dc9ab709f894487f687cbe9aa5;hpb=2eaee49a7ff3ed74598a0db84ce4dbc5bca92380;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/equality_retrieval.mli b/helm/software/components/tactics/paramodulation/equality_retrieval.mli
index e9506580d..7a24e3a55 100644
--- a/helm/software/components/tactics/paramodulation/equality_retrieval.mli
+++ b/helm/software/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 *