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.

1 files changed, 6 insertions, 6 deletions

diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index b4a4a71970..72dcc8c375 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -394,19 +394,19 @@ module Goal : sig
   val env : 'a t -> Environ.env
   val sigma : 'a t -> Evd.evar_map
 
-  (* [enter t] execute the goal-dependent tactic [t] in each goal
+  (* [nf_enter t] execute the goal-dependent tactic [t] in each goal
      independently. In particular [t] need not backtrack the same way in
      each goal. *)
-  val enter : ([ `NF ] t -> unit tactic) -> unit tactic
+  val nf_enter : ([ `NF ] t -> unit tactic) -> unit tactic
 
-  (** Same as enter, but does not normalize the goal beforehand. *)
-  val raw_enter : ([ `LZ ] t -> unit tactic) -> unit tactic
+  (** Same as nf_enter, but does not normalize the goal beforehand. *)
+  val enter : ([ `LZ ] t -> unit tactic) -> unit tactic
 
   (** Recover the list of current goals under focus *)
-  val goals : [ `NF ] t list tactic
+  val nf_goals : [ `NF ] t list tactic
 
   (** Recover the list of current goals under focus, without evar-normalization *)
-  val raw_goals : [ `LZ ] t list tactic
+  val goals : [ `LZ ] t list tactic
 
   (* compatibility: avoid if possible *)
   val goal : [ `NF ] t -> Goal.goal