bugfix: method 'advance' now took in input concrete syntax since atm

[helm.git] / helm / matita / matitaScript.mli

diff --git a/helm/matita/matitaScript.mli b/helm/matita/matitaScript.mli
index cdcb5a544863a5bccc1ebe416108655455e3b334..b1d32eb999774158c6ee6efd0007cc1442b6e28c 100644 (file)
--- 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