diff options
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 22 |
1 files changed, 14 insertions, 8 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 63e1e79db0..59c8992c51 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -584,6 +584,18 @@ let interp_auto_lemmas ist env sigma lems = let pf_interp_type ist gl = interp_type ist (pf_env gl) (project gl) +let new_interp_type ist c = + let open Proofview.Goal in + let open Proofview.Notations in + let interp gl = + try + let (sigma, c) = interp_type ist (env gl) (sigma gl) c in + Proofview.V82.tclEVARS sigma <*> return c + with e when Proofview.V82.catchable_exception e -> + Proofview.tclZERO e + in + enterl interp + (* Interprets a reduction expression *) let interp_unfold ist env (occs,qid) = (interp_occurrences ist occs,interp_evaluable ist env qid) @@ -1577,14 +1589,8 @@ and interp_atomic ist tac = gl end | TacCut c -> - 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) - end + let open Proofview.Notations in + (new_interp_type ist c) >>= Tactics.cut | TacAssert (t,ipat,c) -> Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in |