beginning of the tactics lapply and fwd

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

diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli
index 780961d6b9645ae6114377c87c54839610403d0a..ae9746da1aedea2cf9a1af9535248b78d9d9de2b 100644 (file)
--- a/helm/ocaml/tactics/tactics.mli
+++ b/helm/ocaml/tactics/tactics.mli
@@ -66,3 +66,7 @@ val whd :
 val normalize :
   also_in_hypotheses:bool ->
   terms:Cic.term list option -> ProofEngineTypes.tactic
+val fwd_simpl : hyp:Cic.name -> dbd:Mysql.dbd -> ProofEngineTypes.tactic
+val lapply :
+  ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
+  ?substs:(Cic.name * Cic.term) list -> Cic.term -> ProofEngineTypes.tactic