X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FvariousTactics.ml;h=c1006032471a7d6fffc86959dcedca987c4a05bf;hb=acf29bdbdcdc6ad8c2d9d27e8a47500981b605cd;hp=be08c4d9e9b69bf5114ba1f4c62d6384ea8a312e;hpb=0d729d0fb3fd7c798382e16c1f855ce26edad979;p=helm.git

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index be08c4d9e..c10060324 100644
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -113,4 +113,12 @@ let generalize_tac
   PET.mk_tactic (generalize_tac mk_fresh_name_callback terms)
 ;;
 
+let set_goal n =
+  ProofEngineTypes.mk_tactic
+    (fun (proof, goal) ->
+       let (_, metasenv, _, _) = proof in
+       if CicUtil.exists_meta n metasenv then
+         (proof, [n])
+       else
+         raise (ProofEngineTypes.Fail ("no such meta: " ^ string_of_int n)))