X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Ftactics%2FvariousTactics.mli;h=2b45aa156c39827637ec6a775c577d95917d670c;hb=4c9da07604c4f8b66e4e92861ee38129422d23fb;hp=b80bc352fd5d620285cbac4fd01d59a128e81458;hpb=6bccccbe78dd8ca020038c0d7a901cd5b129fd03;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
-*)
-