From c3a894dbcc32c279b93d7d67d65f888114ae003a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 25 Jul 2005 08:54:23 +0000 Subject: [PATCH] ... --- helm/ocaml/tactics/tactics.mli | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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 -- 2.39.2