X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FinvokeTactics.ml;h=96f306cdf4c8f0b97ce036d17a6d9a2873fee2a2;hb=e974eb6799c994efdee15aa47a34909360dc0aec;hp=d7e71177d5c524904548e6bb3a70d7a0d90ebde5;hpb=7bf5d654c18fee290e7e402800543fe40223c04b;p=helm.git

diff --git a/helm/gTopLevel/invokeTactics.ml b/helm/gTopLevel/invokeTactics.ml
index d7e71177d..96f306cdf 100644
--- a/helm/gTopLevel/invokeTactics.ml
+++ b/helm/gTopLevel/invokeTactics.ml
@@ -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)