X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fdeclarative.mli;h=8fd91b0e853f9c4a83c35d9604de5518aea571d9;hb=b0a6c05decc9f0e731f70cfc5ae5350ae4046b79;hp=97514b684b64bf8486b4fb8ddc9c8732c7ca40e5;hpb=15417a6cd2d1ce39afc67d36436864978ec7a8e2;p=helm.git

diff --git a/components/tactics/declarative.mli b/components/tactics/declarative.mli
index 97514b684..8fd91b0e8 100644
--- a/components/tactics/declarative.mli
+++ b/components/tactics/declarative.mli
@@ -57,5 +57,5 @@ 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 ] ->
+   [ `Term of Cic.term | `Auto of (string * string) list | `Proof ] ->
     bool (* last step *) -> ProofEngineTypes.tactic