From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 25 Jul 2005 08:54:23 +0000 (+0000)
Subject: ...
X-Git-Tag: V_0_7_2~96
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c3a894dbcc32c279b93d7d67d65f888114ae003a;p=helm.git

...
---

diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli
index 5baeeb33c..76f1e89d2 100644
--- 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