diff options
| -rw-r--r-- | tactics/tacinterp.ml | 4 |
1 files changed, 1 insertions, 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 |