X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FvariousTactics.mli;h=2b45aa156c39827637ec6a775c577d95917d670c;hb=7bf5d654c18fee290e7e402800543fe40223c04b;hp=b80bc352fd5d620285cbac4fd01d59a128e81458;hpb=a3ef256812f0397a871fe8e69c125dfd89e62dce;p=helm.git

diff --git a/helm/ocaml/tactics/variousTactics.mli b/helm/ocaml/tactics/variousTactics.mli
index b80bc352f..2b45aa156 100644
--- a/helm/ocaml/tactics/variousTactics.mli
+++ b/helm/ocaml/tactics/variousTactics.mli
@@ -29,9 +29,3 @@ val assumption_tac: ProofEngineTypes.tactic
 val generalize_tac:
  ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> Cic.term list ->
   ProofEngineTypes.tactic
-
-(*
-val decide_equality_tac: ProofEngineTypes.tactic
-val compare_tac: term1:Cic.term -> term2:Cic.term -> ProofEngineTypes.tactic
-*)
-