ocaml 3.09 transition

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

diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli
index 8ea9f641c08932c13e5f75a73bd9b6fb75f3045d..6d524093569a91663c8f57ec091286a756e31350 100644 (file)
--- 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