From 46404f724772c4c1f06c1d8b8d1e3686ca40a28a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 6 Sep 2014 23:48:47 +0200
Subject: Code simplification in Tacinterp.

---
 tactics/tacinterp.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 0077f05686..abf9b900ca 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1199,12 +1199,10 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
               in
               list_unpack { list_unpacker } x
           | ExtraArgType _ ->
-              let (>>=) = Ftactic.bind in
               (** Special treatment of tactics *)
               if has_type x (glbwit wit_tactic) then
                 let tac = out_gen (glbwit wit_tactic) x in
-                val_interp ist tac >>= fun v ->
-                Ftactic.return v
+                val_interp ist tac
               else
                 let goal = Proofview.Goal.goal gl in
                 let (newsigma,v) = Geninterp.generic_interp ist {Evd.it=goal;sigma} x in
-- 
cgit v1.2.3