X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngine.mli;h=cbe4c8bc5b5c5d0584f34bac645992c914812114;hb=850b1a2e1b00104239484ac25aef29c0b943e1e5;hp=c3b623c08654563f9e96b3c9659949f54949d6c6;hpb=3066e4dcb7270a5eb20020a91d45da9eb87e2f2e;p=helm.git

diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli
index c3b623c08..cbe4c8bc5 100644
--- a/helm/gTopLevel/proofEngine.mli
+++ b/helm/gTopLevel/proofEngine.mli
@@ -60,3 +60,16 @@ val elim_type : Cic.term -> unit
 val ring : unit -> unit
 val fourier : unit -> unit
 val rewrite_simpl : Cic.term -> unit
+
+val reflexivity : unit -> unit
+val symmetry : unit -> unit
+val transitivity : Cic.term -> unit
+
+val left : unit -> unit
+val right : unit -> unit
+
+val assumption : unit -> unit
+
+(*
+val prova_tatticali : unit -> unit
+*)