From c720c4687a4290cfb85f6c4d2a9f238450ef0d5a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 9 Jun 2005 16:22:51 +0000 Subject: [PATCH] Error message improved. --- helm/matita/matitaEngine.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) 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 -- 2.39.2