X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FautoTactic.mli;h=fe72629f02ba338155cfee7eadea102410177954;hb=cbac948d507d74a558ba7f11ce10bc252b1ba8ba;hp=e2f20f787f06c4b36ec70a98dca0d9e50824fd52;hpb=259a4a2080cc5af5b20da1cd9133eb32f28c5d8f;p=helm.git

diff --git a/helm/ocaml/tactics/autoTactic.mli b/helm/ocaml/tactics/autoTactic.mli
index e2f20f787..fe72629f0 100644
--- a/helm/ocaml/tactics/autoTactic.mli
+++ b/helm/ocaml/tactics/autoTactic.mli
@@ -25,13 +25,7 @@
  *)
 
 val auto_tac:
-  ?depth:int -> ?width:int -> ?paramodulation:string ->
+  ?depth:int -> ?width:int -> ?paramodulation:string -> ?full:string ->
   dbd:HMysql.dbd -> unit ->
   ProofEngineTypes.tactic
 
-val paramodulation_tactic:
-  (HMysql.dbd -> ProofEngineTypes.status ->
-     ProofEngineTypes.proof * ProofEngineTypes.goal list) ref
-
-val term_is_equality:
-  (Cic.term -> bool) ref