From 521a7b96c8963428ca0ecb39a22f458bf603ccab Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 6 Sep 2014 17:09:51 +0200
Subject: Renaming goal-entering functions.

1. Proofview.Goal.enter into Proofview.Goal.nf_enter.
2. Proofview.Goal.raw_enter into Proofview.Goal.enter.
3. Proofview.Goal.goals -> Proofview.Goals.nf_goals
4. Proofview.Goal.raw_goals -> Proofview.Goals.goals
5. Ftactic.goals -> Ftactic.nf_goals
6. Ftactic.raw_goals -> Ftactic.goals

This is more uniform with the other functions of Coq.
---
 proofs/tactic_debug.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs/tactic_debug.ml')

diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 62b157307a..19a1f77584 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
-- 
cgit v1.2.3