diff options
| -rw-r--r-- | tactics/tacinterp.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 4b0bf1faed..e0d24e9e1b 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1048,14 +1048,13 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacMatchGoal _ | TacMatch _ -> assert false | TacId s -> Proofview.tclTHEN - (Proofview.Goal.enter begin fun gl -> + (Proofview.tclENV >>= fun env -> let msg = - try Proofview.tclUNIT (interp_message_nl ist (Proofview.Goal.env gl) s) + try Proofview.tclUNIT (interp_message_nl ist env s) with e when Errors.noncritical e -> Proofview.tclZERO e in msg >>= fun msg -> - Proofview.tclLIFT (Proofview.NonLogical.print (Pp.hov 0 msg)) - end) + Proofview.tclLIFT (Proofview.NonLogical.print (Pp.hov 0 msg))) (Proofview.tclLIFT (db_breakpoint (curr_debug ist) s)) | TacFail (n,s) -> Proofview.V82.tactic begin fun gl -> |