merged changes from the svn fork by me and Enrico

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

diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli
index 7b771249e6bf6d8cfeba903b2061e5f82cb5eaef..d70c94ac54f39a057b0b4bb7d414bb2b35e0cccd 100644 (file)
--- a/helm/ocaml/tactics/tactics.mli
+++ b/helm/ocaml/tactics/tactics.mli
@@ -32,6 +32,7 @@ val fourier : ProofEngineTypes.tactic
 val generalize :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
   Cic.term list -> ProofEngineTypes.tactic
+val set_goal : int -> ProofEngineTypes.tactic
 val injection : term:Cic.term -> ProofEngineTypes.tactic
 val intros :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->