diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-06 23:48:47 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-06 23:48:47 +0200 |
| commit | 46404f724772c4c1f06c1d8b8d1e3686ca40a28a (patch) | |
| tree | 3962717bc0049569c95c6d0b8300c7d4c90cff1f /tactics | |
| parent | a74074a8133ad954dff54bee190dbaa5332564a0 (diff) | |
Code simplification in Tacinterp.
Diffstat (limited to 'tactics')
| -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 0077f0568..abf9b900c 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 |