diff options
Diffstat (limited to 'ltac/tacinterp.ml')
| -rw-r--r-- | ltac/tacinterp.ml | 14 |
1 files changed, 0 insertions, 14 deletions
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index c51c36538d..5ee9b0fc4d 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1800,20 +1800,6 @@ and interp_atomic ist tac : unit Proofview.tactic = in Sigma.Unsafe.of_pair (tac, sigma) end } - (* Context management *) - | TacRename l -> - Proofview.Goal.enter { enter = begin fun gl -> - let env = pf_env gl in - let sigma = project gl in - let l = - List.map (fun (id1,id2) -> - interp_hyp ist env sigma id1, - interp_ident ist env sigma (snd id2)) l - in - name_atomic ~env - (TacRename l) - (Tactics.rename_hyp l) - end } (* Conversion *) | TacReduce (r,cl) -> |