GtkHSeparator deprecated

[helm.git] / helm / software / components / tactics / auto.mli

diff --git a/helm/software/components/tactics/auto.mli b/helm/software/components/tactics/auto.mli
index d5297e7b84eddfe62e7bd995356be43045b81e00..557d78194dcf7d82e2f39df30fb21414910718be 100644 (file)
--- 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) *)