Less use of the list-based interface for goal-bound tactics.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17002 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 8 deletions

diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index dc48cfc3bc..1cc08fa49b 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -42,22 +42,20 @@ let msg_tac_debug s = Proofview.NonLogical.print (s++fnl())
 
 (* Prints the goal *)
 
-let db_pr_goal =
-  let (>>=) = Goal.bind in
-  Goal.env >>= fun env ->
-  Goal.concl >>= fun concl ->
+let db_pr_goal gl =
+  let env = Proofview.Goal.env gl in
+  let concl = Proofview.Goal.concl gl in
   let penv = print_named_context env in
   let pc = print_constr_env env concl in
-  Goal.return begin
     str"  " ++ hv 0 (penv ++ fnl () ++
                    str "============================" ++ fnl ()  ++
                    str" "  ++ pc) ++ fnl ()
-  end
 
 let db_pr_goal =
-  let (>>=) = Proofview.Notations.(>>=) in
-  Proofview.Goal.lift db_pr_goal >>= fun pg ->
+  Proofview.Goal.enter begin fun gl ->
+  let pg = db_pr_goal gl in
   Proofview.tclLIFT (msg_tac_debug (str "Goal:" ++ fnl () ++ pg))
+  end
 
 
 (* Prints the commands *)