]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaGui.ml
New argument (the hypothesis name) for cut.
[helm.git] / helm / matita / matitaGui.ml
index 8eec3244d29915ff57768b0acb1f0de7961c2cc4..e2b4d4682830a4950793421987a1048d370b9521 100644 (file)
@@ -167,7 +167,7 @@ class gui () =
       connect_button tbar#transitivityButton
         (tac_w_term (A.Transitivity (loc, hole)));
       connect_button tbar#assumptionButton (tac (A.Assumption loc));
-      connect_button tbar#cutButton (tac_w_term (A.Cut (loc, hole)));
+      connect_button tbar#cutButton (tac_w_term (A.Cut (loc, None, hole)));
       connect_button tbar#autoButton (tac (A.Auto (loc,None,None)));
       MatitaGtkMisc.toggle_widget_visibility
        ~widget:(self#main#tacticsButtonsHandlebox :> GObj.widget)