Added variousTactic with Constructor, Left, Right, Exists, Reflexivity, Symmetry...

[helm.git] / helm / gTopLevel / proofEngine.mli

diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli
index c3b623c08654563f9e96b3c9659949f54949d6c6..cbe4c8bc5b5c5d0584f34bac645992c914812114 100644 (file)
--- 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
+*)