Constructors are closed with thier types when computing the signatur

[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..c8a9224cb9fec6266e1388a469e0ebcf23645a39 100644 (file)
--- 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) *)