]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/invokeTactics.ml
Added buttons for new tactics Injection and Discriminate
[helm.git] / helm / gTopLevel / invokeTactics.ml
index 5e75b5b2d9647d057f20e64aabbe1df031f1d516..96f306cdf4c8f0b97ce036d17a6d9a2873fee2a2 100644 (file)
@@ -319,7 +319,7 @@ module Make(C:Callbacks) =
      match scratch_window#sequent_viewer#get_selected_terms with
         [] ->
          C.output_html
-          ("<h1 color=\"red\">No term selected</h1>")
+          ("<h1 color=\"red\">No terms selected</h1>")
       | terms ->
          try
           let expr = tactic terms scratch_window#term in
@@ -409,6 +409,8 @@ module Make(C:Callbacks) =
   let left = call_tactic ProofEngine.left
   let right = call_tactic ProofEngine.right
   let assumption = call_tactic ProofEngine.assumption
+  let injection = call_tactic_with_input ProofEngine.injection
+  let discriminate = call_tactic_with_input ProofEngine.discriminate
   let generalize =
    call_tactic_with_goal_inputs
     (ProofEngine.generalize ~mk_fresh_name_callback:C.mk_fresh_name_callback)