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

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

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 972ae962afa3805ea0de092df33f0733809dd3b0..b47f8856a682581d2a32d0ae18e984ea5a975810 100644 (file)
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -288,3 +288,16 @@ let elim_type term = apply_tactic (Ring.elim_type_tac ~term)
 let ring () = apply_tactic Ring.ring_tac
 let fourier () = apply_tactic FourierR.fourier_tac
 let rewrite_simpl term = apply_tactic (FourierR.rewrite_simpl_tac ~term)
+
+let reflexivity () = apply_tactic VariousTactics.reflexivity_tac
+let symmetry () = apply_tactic VariousTactics.symmetry_tac
+let transitivity term = apply_tactic (VariousTactics.transitivity_tac ~term)
+
+let left () = apply_tactic VariousTactics.left_tac
+let right () = apply_tactic VariousTactics.right_tac
+
+let assumption () = apply_tactic VariousTactics.assumption_tac
+(*
+let prova_tatticali () = apply_tactic Tacticals.prova_tac
+*)
+