diff options
| author | Pierre-Marie Pédrot | 2014-03-07 21:30:54 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-03-07 21:30:54 +0100 |
| commit | 1f4c7b799235860808a0aeb40afb40df64b7367e (patch) | |
| tree | 2e3165b05d4b8d2867e3729c582c037aed21247c | |
| parent | dd2a0175e3e35e5488c6f3b8a68c68845cbfcfd3 (diff) | |
Useless tactic bindings in Tacticals.
| -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 |