X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=8aae7633a9222fd8f8dc86b0a3d737369827492b;hb=de9c41f0dba38ec7c8b9459ef2eb3844660c0b35;hp=eb3193264edf260dd716eafa597669bfc80c8069;hpb=a092d97f720a9241d77d987a72cdb810c1d88212;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index eb3193264..8aae7633a 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -654,9 +654,8 @@ let disambiguate_executable status ex =
       let status, cmd = disambiguate_command status cmd in
       status, (TacticAst.Command (loc, cmd))
   | TacticAst.Macro (_, mac) -> 
-      command_error 
-        (sprintf ("The engine is not allowed to disambiguate any macro, "^^
-                 "in particular %s") (TacticAstPp.pp_macro_ast mac))
+      command_error (sprintf "The macro %s can't be in a script" 
+        (TacticAstPp.pp_macro_ast mac))
 
 let disambiguate_comment status c = 
   match c with