diff options
| -rw-r--r-- | tactics/tacticals.ml | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index c6a3a0012d..dd344ee3d9 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -555,13 +555,9 @@ module New = struct mkVar (nthHypId m gl) let onNthHypId m tac = - Goal.enter begin fun gl -> - Proofview.tclUNIT (nthHypId m gl) >>= tac - end + Proofview.Goal.enter begin fun gl -> tac (nthHypId m gl) end let onNthHyp m tac = - Goal.enter begin fun gl -> - Proofview.tclUNIT (nthHyp m gl) >>= tac - end + Proofview.Goal.enter begin fun gl -> tac (nthHyp m gl) end let onLastHypId = onNthHypId 1 let onLastHyp = onNthHyp 1 |