diff options
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 81fbcc6db6..65fdecc29b 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1894,18 +1894,6 @@ and interp_atomic ist tac : unit Proofview.tactic = (Tactics.rename_hyp l) end } - (* Constructors *) - | TacSplit (ev,bll) -> - Proofview.Goal.enter { enter = begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = project gl in - let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in - let named_tac = - let tac = Tactics.split_with_bindings ev bll in - name_atomic ~env (TacSplit (ev, bll)) tac - in - Tacticals.New.tclWITHHOLES ev named_tac sigma - end } (* Conversion *) | TacReduce (r,cl) -> (* spiwack: until the tactic is in the monad *) |