From cc42541eeaaec0371940e07efdb009a4ee74e468 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 20 Oct 2015 13:04:45 +0200
Subject: Boxing the Goal.enter primitive into a record type.

---
 proofs/tactic_debug.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'proofs/tactic_debug.ml')

diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 6d6215c521..fb23a28feb 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -12,6 +12,7 @@ open Pp
 open Tacexpr
 open Termops
 open Nameops
+open Proofview.Notations
 
 let (prtac, tactic_printer) = Hook.make ()
 let (prmatchpatt, match_pattern_printer) = Hook.make ()
@@ -47,10 +48,10 @@ let db_pr_goal gl =
                    str" "  ++ pc) ++ fnl ()
 
 let db_pr_goal =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
   let pg = db_pr_goal gl in
   Proofview.tclLIFT (msg_tac_notice (str "Goal:" ++ fnl () ++ pg))
-  end
+  end }
 
 
 (* Prints the commands *)
-- 
cgit v1.2.3