A few other tactics made available to matita.

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

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 9fcbb966fc2d9ae3072df98935d31bbdb1059fd7..226a8c87c831d29531078d1d56707ec3e9a919e0 100644 (file)
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -131,13 +131,3 @@ let generalize_tac
  in
   PET.mk_tactic (generalize_tac mk_fresh_name_callback ~term pattern)
 ;;
-
-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)))
-