From f931b170b3be3da2e2c245c566aad2b483223a51 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 25 Feb 2014 12:32:34 +0100
Subject: Tacinterp: remove unnecessary return/bind pairs.

---
 tactics/tacinterp.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a8180f4929..3dd42e0e54 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1994,12 +1994,14 @@ and interp_atomic ist tac =
               Proofview.Goal.return (mk_hyp_value ist env (out_gen (glbwit wit_var) x))
           | GenArgType -> f (out_gen (glbwit wit_genarg) x)
           | ConstrArgType ->
-              Proofview.Goal.return (Tacmach.New.of_old (fun gl -> mk_constr_value ist gl (out_gen (glbwit wit_constr) x)) gl) >>== fun (sigma,v) ->
+              let (sigma,v) =
+                Tacmach.New.of_old (fun gl -> mk_constr_value ist gl (out_gen (glbwit wit_constr) x)) gl
+              in
               (Proofview.V82.tclEVARS sigma) <*>
 	      (Proofview.Goal.return v)
           | OpenConstrArgType ->
-              Proofview.Goal.return (
-                Tacmach.New.of_old (fun gl -> mk_open_constr_value ist gl (snd (out_gen (glbwit wit_open_constr) x))) gl) >>== fun (sigma,v) ->
+              let (sigma,v) =
+                Tacmach.New.of_old (fun gl -> mk_open_constr_value ist gl (snd (out_gen (glbwit wit_open_constr) x))) gl in
               (Proofview.V82.tclEVARS sigma) <*>
 	      (Proofview.Goal.return v)
           | ConstrMayEvalArgType ->
-- 
cgit v1.2.3