X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Ftactics.mli;h=6d524093569a91663c8f57ec091286a756e31350;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=8ea9f641c08932c13e5f75a73bd9b6fb75f3045d;hpb=259a4a2080cc5af5b20da1cd9133eb32f28c5d8f;p=helm.git

diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli
index 8ea9f641c..6d5240935 100644
--- a/helm/ocaml/tactics/tactics.mli
+++ b/helm/ocaml/tactics/tactics.mli
@@ -5,7 +5,8 @@ val assumption : ProofEngineTypes.tactic
 val auto :
   ?depth:int ->
   ?width:int ->
-  ?paramodulation:string -> dbd:HMysql.dbd -> unit -> ProofEngineTypes.tactic
+  ?paramodulation:string ->
+  ?full:string -> dbd:HMysql.dbd -> unit -> ProofEngineTypes.tactic
 val change :
   pattern:ProofEngineTypes.pattern ->
   ProofEngineTypes.lazy_term -> ProofEngineTypes.tactic