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

diff --git a/helm/gTopLevel/invokeTactics.mli b/helm/gTopLevel/invokeTactics.mli
index d527e4faf..313991ced 100644
--- a/helm/gTopLevel/invokeTactics.mli
+++ b/helm/gTopLevel/invokeTactics.mli
@@ -99,6 +99,8 @@ module Make (C : Callbacks) :
    val absurd : unit -> unit
    val contradiction : unit -> unit
    val decompose : unit -> unit
+   val injection : unit -> unit
+   val discriminate : unit -> unit
    val whd_in_scratch : unit -> unit
    val reduce_in_scratch : unit -> unit
    val simpl_in_scratch : unit -> unit