diff options
| author | Arnaud Spiwack | 2014-02-27 11:20:25 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-02-27 11:20:25 +0100 |
| commit | b1ebce6e811eb6e1d4476b873e13155cc83c5ee1 (patch) | |
| tree | 46f9bd1256429ac4507b7fd40a9df49a941e37ca | |
| parent | 35a0c9b1f7fab940affe676f8b8c5cdd36071172 (diff) | |
Tacinterp: yet another superfluous enterl.
| -rw-r--r-- | tactics/tacinterp.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 3e43942283..171c248584 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -581,11 +581,11 @@ let new_interp_type ist c = let interp gl = try let (sigma, c) = interp_type ist (env gl) (sigma gl) c in - Proofview.V82.tclEVARS sigma <*> return c + Proofview.V82.tclEVARS sigma <*> Proofview.tclUNIT c with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e in - enterl interp + interp (* Interprets a reduction expression *) let interp_unfold ist env (occs,qid) = @@ -1587,7 +1587,9 @@ and interp_atomic ist tac = end | TacCut c -> let open Proofview.Notations in - (new_interp_type ist c) >>= Tactics.cut + Proofview.Goal.enter begin fun gl -> + new_interp_type ist c gl >= Tactics.cut + end | TacAssert (t,ipat,c) -> Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in |