diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-04 12:09:43 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-04 12:57:32 +0200 |
| commit | ba9ba59be9534b42ede74adfcbf8b85b876590c7 (patch) | |
| tree | 13968dc5748fd57edf40e606e96767dcedc5a31c /tactics | |
| parent | 85f440deb8b87fe42a3623bbafd1f78243711a34 (diff) | |
Revert "Ltac's [idtac] is now interpreted outside of a goal if possible."
This reverts commit afa441019432f70245fed6adc5eb0318514e4357.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index e69a307bd..df79361fe 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1102,13 +1102,14 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacMatchGoal _ | TacMatch _ -> assert false | TacId s -> Proofview.tclTHEN - (Proofview.tclENV >>= fun env -> + (Proofview.Goal.enter begin fun gl -> let msg = - try Proofview.tclUNIT (interp_message_nl ist env s) + try Proofview.tclUNIT (interp_message_nl ist (Proofview.Goal.env gl) s) with e when Errors.noncritical e -> Proofview.tclZERO e in msg >>= fun msg -> - Proofview.tclLIFT (Proofview.NonLogical.print (Pp.hov 0 msg))) + Proofview.tclLIFT (Proofview.NonLogical.print (Pp.hov 0 msg)) + end) (Proofview.tclLIFT (db_breakpoint (curr_debug ist) s)) | TacFail (n,s) -> Proofview.V82.tactic begin fun gl -> |