added applyS

[helm.git] / components / tactics / autoTactic.mli

diff --git a/components/tactics/autoTactic.mli b/components/tactics/autoTactic.mli
index fe72629f02ba338155cfee7eadea102410177954..2070116488d577308330a210a0c860f0fd53bfe9 100644 (file)
--- a/components/tactics/autoTactic.mli
+++ b/components/tactics/autoTactic.mli
@@ -29,3 +29,4 @@ val auto_tac:
   dbd:HMysql.dbd -> unit ->
   ProofEngineTypes.tactic
 
+val applyS_tac: dbd:HMysql.dbd -> term: Cic.term -> ProofEngineTypes.tactic