X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.mli;h=557d78194dcf7d82e2f39df30fb21414910718be;hb=a149b1474110583ea5f47fa5bcb85554bba92f19;hp=d5297e7b84eddfe62e7bd995356be43045b81e00;hpb=b4f6b1a39b59e923527f5c17d8fdd0fa1e13e1bf;p=helm.git

diff --git a/helm/software/components/tactics/auto.mli b/helm/software/components/tactics/auto.mli
index d5297e7b8..557d78194 100644
--- a/helm/software/components/tactics/auto.mli
+++ b/helm/software/components/tactics/auto.mli
@@ -23,7 +23,7 @@
  * http://cs.unibo.it/helm/.
  *)
 
-type auto_params = Cic.term list * (string * string) list 
+type auto_params = Cic.term list option * (string * string) list 
 
 val auto_tac:
   dbd:HSql.dbd -> 
@@ -49,11 +49,6 @@ val demodulate_theorem :
   UriManager.uri -> 
   Cic.term * Cic.term
 
-val solve_rewrite_tac:
-  params:auto_params ->
-  automation_cache:AutomationCache.cache ->
-  unit -> ProofEngineTypes.tactic
-
 type auto_status = 
   Cic.context * 
   (* or list: goalno, goaltype, grey, depth, candidates: (goalno, c) *)