Much ado about nothing:

[helm.git] / matita / matitaGui.ml

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index 684e1fa2f3d40f9dc182326175f6db07fd0d5bc7..55db1774cde3e4818ae5bf468082b046a95afe8e 100644 (file)
--- a/matita/matitaGui.ml
+++ b/matita/matitaGui.ml
@@ -973,8 +973,8 @@ class gui () =
         if (MatitaScript.current ())#onGoingProof () then
           (MatitaScript.current ())#advance
             ~statement:("\n"
-              ^ GrafiteAstPp.pp_tactical ~term_pp:CicNotationPp.pp_term
-                ~lazy_term_pp:CicNotationPp.pp_term (A.Tactic (loc, ast)))
+              ^ GrafiteAstPp.pp_tactic ~term_pp:CicNotationPp.pp_term
+                ~lazy_term_pp:CicNotationPp.pp_term ast)
             ()
       in
       let tac_w_term ast _ =