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.
---
 grammar/tacextend.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'grammar')

diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index dd00bc19a5..aec115b7ef 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -189,7 +189,7 @@ let declare_tactic loc s c cl = match cl with
   let name = mlexpr_of_string name in
   let tac =
     (** Special handling of tactics without arguments: such tactics do not do
-        a Proofview.Goal.enter to compute their arguments. It matters for some
+        a Proofview.Goal.nf_enter to compute their arguments. It matters for some
         whole-prof tactics like [shelve_unifiable]. *)
     if List.is_empty rem then
       <:expr< fun _ $lid:"ist"$ -> $tac$ >>
-- 
cgit v1.2.3