aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/tactic_debug.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/tactic_debug.ml')
-rw-r--r--proofs/tactic_debug.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 62b157307..19a1f7758 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -52,7 +52,7 @@ let db_pr_goal gl =
str" " ++ pc) ++ fnl ()
let db_pr_goal =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let pg = db_pr_goal gl in
Proofview.tclLIFT (msg_tac_debug (str "Goal:" ++ fnl () ++ pg))
end