X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fdeclarative.mli;h=08852c79cf70334bb4f9509e33ec0e37eca6f0e7;hb=18758ebe381286b4aff2232e837a0256c00b400b;hp=8fd91b0e853f9c4a83c35d9604de5518aea571d9;hpb=ca2a604c2817deb118d595611b94a0d77978eab6;p=helm.git

diff --git a/helm/software/components/tactics/declarative.mli b/helm/software/components/tactics/declarative.mli
index 8fd91b0e8..08852c79c 100644
--- a/helm/software/components/tactics/declarative.mli
+++ b/helm/software/components/tactics/declarative.mli
@@ -57,5 +57,6 @@ val andelim :
 val rewritingstep :
  dbd:HSql.dbd -> universe:Universe.universe ->
   (string option * Cic.term) option -> Cic.term ->
-   [ `Term of Cic.term | `Auto of (string * string) list | `Proof ] ->
+   [ `Term of Cic.term | `Auto of Auto.auto_params
+   | `Proof  | `SolveWith of Cic.term] ->
     bool (* last step *) -> ProofEngineTypes.tactic