elim tactic: now takes a pattern instead of just a term

[helm.git] / matita / matitaGui.ml

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index a9faa592e8de974b5ce3192a81eacf22f556ac0c..83fee2e1565628013e8ad8ee60fefc2bfacedaae 100644 (file)
--- a/matita/matitaGui.ml
+++ b/matita/matitaGui.ml
@@ -990,7 +990,7 @@ 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, [])));
+        (A.Elim (loc, (Some hole, [], Some CicNotationPt.UserInput), None, None, [])));
       connect_button tbar#elimTypeButton (tac_w_term
         (A.ElimType (loc, hole, None, None, [])));
       connect_button tbar#splitButton (tac (A.Split loc));