Never implemented tactics compare and decide equality purged from the code.

[helm.git] / components / tactics / tactics.mli

diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli
index c8c225cddd2ae8a8015f8d3b241aecffa23c635b..211897a8a02506c76357869294f97338d9c1bb35 100644 (file)
--- 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 ->