"Insert Query (Experts only)" menu item added.

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

diff --git a/helm/gTopLevel/variousTactics.mli b/helm/gTopLevel/variousTactics.mli
index 660ac17f5e518ed26129f1da15ce7298a8ed8444..27b59682f45a4a4c1f7031b7445f8098db928b49 100644 (file)
--- a/helm/gTopLevel/variousTactics.mli
+++ b/helm/gTopLevel/variousTactics.mli
@@ -23,18 +23,12 @@
  * http://cs.unibo.it/helm/.
  *)
 
-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
-val right_tac: ProofEngineTypes.tactic
-
 val assumption_tac: ProofEngineTypes.tactic
 
+val generalize_tac: term:Cic.term -> 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
 *)
+