Much ado about nothing:

[helm.git] / matita / matitaGui.ml

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index a9faa592e8de974b5ce3192a81eacf22f556ac0c..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 _ =
@@ -990,7 +990,8 @@ class gui () =
       connect_button tbar#applyButton (tac_w_term (A.Apply (loc, hole)));
       connect_button tbar#exactButton (tac_w_term (A.Exact (loc, hole)));
       connect_button tbar#elimButton (tac_w_term
-        (A.Elim (loc, hole, None, None, [])));
+        (let pattern = None, [], Some CicNotationPt.UserInput in
+       A.Elim (loc, hole, None, pattern, None, [])));
       connect_button tbar#elimTypeButton (tac_w_term
         (A.ElimType (loc, hole, None, None, [])));
       connect_button tbar#splitButton (tac (A.Split loc));