From 88685adce112ba14de5051e1d40f0b203dfc2922 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 10 Feb 2005 15:44:20 +0000 Subject: [PATCH] bugfix: avoid executing tactic for the script twice --- helm/matita/matita.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index e6eff09fe..59ec55f3a 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -105,7 +105,7 @@ let console_callback s = in let ast = disambiguator#parserr#parseTactical (Stream.of_string s) in if needed_by_script ast then - script#advance ast + script#advance s else interpreter#evalAst ast @@ -138,8 +138,7 @@ let _ = let hole = CicAst.UserInput in let tac ast _ = let ast = A.Tactic ast in - ignore (interpreter#evalAst ast); - ignore (script#advance ast) + ignore (script#advance (TacticAstPp.pp_tactical ast)) in let tac_w_term ast _ = (* gui#console#clear (); *) -- 2.39.2