X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FvariousTactics.mli;h=30887a60af12a4762399a19045cfd9e446827a7b;hb=086c66b6682a49fec4041c25e741b2736f385e6a;hp=660ac17f5e518ed26129f1da15ce7298a8ed8444;hpb=373eaf73bebec626e031a4a534ddfdd4f1c1b474;p=helm.git

diff --git a/helm/gTopLevel/variousTactics.mli b/helm/gTopLevel/variousTactics.mli
index 660ac17f5..30887a60a 100644
--- a/helm/gTopLevel/variousTactics.mli
+++ b/helm/gTopLevel/variousTactics.mli
@@ -27,7 +27,9 @@ val reflexivity_tac: ProofEngineTypes.tactic
 val symmetry_tac: ProofEngineTypes.tactic
 val transitivity_tac: term:Cic.term -> ProofEngineTypes.tactic
 
+(*
 val constructor_tac: n:int -> ProofEngineTypes.tactic
+*)
 val exists_tac: ProofEngineTypes.tactic
 val split_tac: ProofEngineTypes.tactic
 val left_tac: ProofEngineTypes.tactic
@@ -35,6 +37,21 @@ val right_tac: ProofEngineTypes.tactic
 
 val assumption_tac: ProofEngineTypes.tactic
 
+val generalize_tac: term:Cic.term -> ProofEngineTypes.tactic
+
+val elim_type_tac: term:Cic.term -> ProofEngineTypes.tactic
+
+val absurd_tac: term:Cic.term -> ProofEngineTypes.tactic
+val contradiction_tac: ProofEngineTypes.tactic
+
+val decompose_tac: clist:(Cic.term list) -> ProofEngineTypes.tactic
+
 (*
-val generalize_tac: Cic.term -> ProofEnginrTypes.tactic
+val decide_equality_tac: ProofEngineTypes.tactic
+val compare_tac: term1:Cic.term -> term2:Cic.term -> ProofEngineTypes.tactic
 *)
+
+val rewrite_tac: term:Cic.term -> ProofEngineTypes.tactic
+val rewrite_simpl_tac: term:Cic.term -> ProofEngineTypes.tactic
+val rewrite_back_tac: term:Cic.term -> ProofEngineTypes.tactic
+val replace_tac: what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic