Much ado about nothing:

[helm.git] / components / tactics / proofEngineStructuralRules.ml

diff --git a/components/tactics/proofEngineStructuralRules.ml b/components/tactics/proofEngineStructuralRules.ml
index 3db6d4ff3970fde33c680a56634d6e362931ac5f..636ea07c0f3c67d36ba04ae3dc4057a6de4b14e5 100644 (file)
--- a/components/tactics/proofEngineStructuralRules.ml
+++ b/components/tactics/proofEngineStructuralRules.ml
@@ -194,12 +194,3 @@ let rename ~froms ~tos =
       (curi, metasenv, pbo, pty, attrs), [goal]
    in
    PET.mk_tactic rename
-
-let set_goal n =
-  PET.mk_tactic
-    (fun (proof, goal) ->
-       let (_, metasenv, _, _, _) = proof in
-       if CicUtil.exists_meta n metasenv then
-         (proof, [n])
-       else
-         raise (PET.Fail (lazy ("no such meta: " ^ string_of_int n))))