X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Ftactics.mli;h=211897a8a02506c76357869294f97338d9c1bb35;hb=db8577d788a84ecb10eb59e70bed233fc159d2f6;hp=c8c225cddd2ae8a8015f8d3b241aecffa23c635b;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli
index c8c225cdd..211897a8a 100644
--- a/components/tactics/tactics.mli
+++ b/components/tactics/tactics.mli
@@ -12,13 +12,11 @@ val change :
   Cic.lazy_term -> ProofEngineTypes.tactic
 val clear : hyp:string -> ProofEngineTypes.tactic
 val clearbody : hyp:string -> ProofEngineTypes.tactic
-val compare : term:Cic.term -> ProofEngineTypes.tactic
 val constructor : n:int -> ProofEngineTypes.tactic
 val contradiction : ProofEngineTypes.tactic
 val cut :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
   Cic.term -> ProofEngineTypes.tactic
-val decide_equality : ProofEngineTypes.tactic
 val decompose :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
   ?user_types:(UriManager.uri * int) list ->