merged changes from the svn fork by me and Enrico

[helm.git] / helm / ocaml / tactics / variousTactics.ml

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index be08c4d9e9b69bf5114ba1f4c62d6384ea8a312e..c1006032471a7d6fffc86959dcedca987c4a05bf 100644 (file)
--- 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)))