X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.mli;h=c8a9224cb9fec6266e1388a469e0ebcf23645a39;hb=5d0d8107649b9264ebe7d8ff2c69bf777179b0d2;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..c8a9224cb 100644
--- a/helm/software/components/tactics/auto.mli
+++ b/helm/software/components/tactics/auto.mli
@@ -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) *)