diff options
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index e5f69378f4..63e1e79db0 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1577,12 +1577,13 @@ and interp_atomic ist tac = gl end | TacCut c -> - Proofview.V82.tactic begin fun gl -> - let (sigma,c_interp) = pf_interp_type ist gl c in - tclTHEN - (tclEVARS sigma) + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let (sigma, c_interp) = interp_type ist env sigma c in + Tacticals.New.tclTHEN + (Proofview.V82.tclEVARS sigma) (Tactics.cut c_interp) - gl end | TacAssert (t,ipat,c) -> Proofview.Goal.enter begin fun gl -> |