From 1f4c7b799235860808a0aeb40afb40df64b7367e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 7 Mar 2014 21:30:54 +0100
Subject: Useless tactic bindings in Tacticals.

---
 tactics/tacticals.ml | 8 ++------
 1 file 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
-- 
cgit v1.2.3