X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaScript.mli;h=b1d32eb999774158c6ee6efd0007cc1442b6e28c;hb=0aaed6f96b856d1181a3cd1f2ef3ea4a91990771;hp=cdcb5a544863a5bccc1ebe416108655455e3b334;hpb=642e20a0135126586603ffb539f0d1c1428f1502;p=helm.git

diff --git a/helm/matita/matitaScript.mli b/helm/matita/matitaScript.mli
index cdcb5a544..b1d32eb99 100644
--- a/helm/matita/matitaScript.mli
+++ b/helm/matita/matitaScript.mli
@@ -38,7 +38,7 @@ class type script =
       (** adds a tactical at current script execution point and execute it. Used
       * when the user uses buttons or console instead of directly editing the
       * script *)
-    method advance: DisambiguateTypes.tactical -> MatitaTypes.command_outcome
+    method advance: string -> MatitaTypes.command_outcome
   end
 
 val script: interpreter:MatitaTypes.interpreter -> script