...

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

diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli
index 5baeeb33c61b44c07067d96ce2aeefa6aed37947..76f1e89d2ffec438d3971c3784d0e81e13348198 100644 (file)
--- a/helm/ocaml/tactics/tactics.mli
+++ b/helm/ocaml/tactics/tactics.mli
@@ -4,7 +4,8 @@ val apply : term:Cic.term -> ProofEngineTypes.tactic
 val assumption : ProofEngineTypes.tactic
 val auto :
   ?depth:int ->
-  ?width:int -> dbd:Mysql.dbd -> unit -> ProofEngineTypes.tactic
+  ?width:int ->
+  ?paramodulation:string -> dbd:Mysql.dbd -> unit -> ProofEngineTypes.tactic
 val change :
   pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic
 val clear : hyp:string -> ProofEngineTypes.tactic