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.

4 files changed, 21 insertions, 21 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 589cb5bdaa..d4826ce202 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -83,7 +83,7 @@ open Unification
 let dft = default_unify_flags
 
 let res_pf ?(with_evars=false) ?(flags=dft ()) clenv =
-  Proofview.Goal.raw_enter begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let clenv gl = clenv_unique_resolver ~flags clenv gl in
     clenv_refine with_evars (Tacmach.New.of_old clenv (Proofview.Goal.assume gl))
   end
@@ -112,7 +112,7 @@ let fail_quick_unif_flags = {
 
 (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
 let unify ?(flags=fail_quick_unif_flags) m =
-  Proofview.Goal.raw_enter begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let env = Tacmach.New.pf_env gl in
     let n = Tacmach.New.pf_nf_concl gl in
     let evd = create_goal_evar_defs (Proofview.Goal.sigma gl) in
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 506d04f38a..48ca848915 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -848,40 +848,40 @@ module Goal = struct
   let hyps { env=env } = Environ.named_context env
   let concl { concl=concl } = concl
 
-  let enter_t = Goal.nf_enter begin fun env sigma concl self ->
+  let nf_enter_t = Goal.nf_enter begin fun env sigma concl self ->
     {env=env;sigma=sigma;concl=concl;self=self}
   end
 
-  let enter f =
+  let nf_enter f =
     list_iter_goal () begin fun goal () ->
       Proof.current >>= fun env ->
       tclEVARMAP >>= fun sigma ->
       try
-        let (gl, sigma) = Goal.eval enter_t env sigma goal in
+        let (gl, sigma) = Goal.eval nf_enter_t env sigma goal in
         tclTHEN (V82.tclEVARS sigma) (f gl)
       with e when catchable_exception e ->
         let e = Errors.push e in
         tclZERO e
     end
 
-  let raw_enter_t f = Goal.enter begin fun env sigma concl self ->
+  let enter_t f = Goal.enter begin fun env sigma concl self ->
     f {env=env;sigma=sigma;concl=concl;self=self}
   end
 
-  let raw_enter f =
+  let enter f =
     list_iter_goal () begin fun goal () ->
       Proof.current >>= fun env ->
       tclEVARMAP >>= fun sigma ->
       try
         (* raw_enter_t cannot modify the sigma. *)
-        let (t,_) = Goal.eval (raw_enter_t f) env sigma goal in
+        let (t,_) = Goal.eval (enter_t f) env sigma goal in
         t
       with e when catchable_exception e ->
         let e = Errors.push e in
         tclZERO e
     end
 
-  let goals =
+  let nf_goals =
     Proof.current >>= fun env ->
     Proof.get >>= fun step ->
     let sigma = step.solution in
@@ -890,12 +890,12 @@ module Goal = struct
       | None -> None (** ppedrot: Is this check really necessary? *)
       | Some goal ->
         (** The sigma is unchanged. *)
-        let (gl, _) = Goal.eval enter_t env sigma goal in
+        let (gl, _) = Goal.eval nf_enter_t env sigma goal in
         Some gl
     in
     tclUNIT (List.map_filter map step.comb)
 
-  let raw_goals =
+  let goals =
     Proof.current >>= fun env ->
     Proof.get >>= fun step ->
     let sigma = step.solution in
@@ -904,7 +904,7 @@ module Goal = struct
       | None -> None (** ppedrot: Is this check really necessary? *)
       | Some goal ->
         (** The sigma is unchanged. *)
-        let (gl, _) = Goal.eval (raw_enter_t (fun gl -> gl)) env sigma goal in
+        let (gl, _) = Goal.eval (enter_t (fun gl -> gl)) env sigma goal in
         Some gl
     in
     tclUNIT (List.map_filter map step.comb)
@@ -963,7 +963,7 @@ struct
     let () = Typing.check env evdref c concl in
     !evdref
 
-  let refine ?(unsafe = false) f = Goal.raw_enter begin fun gl ->
+  let refine ?(unsafe = false) f = Goal.enter begin fun gl ->
     let sigma = Goal.sigma gl in
     let env = Goal.env gl in
     let concl = Goal.concl gl in
@@ -980,7 +980,7 @@ struct
     Proof.set { solution = sigma; comb; }
   end
 
-  let refine_casted ?(unsafe = false) f = Goal.raw_enter begin fun gl ->
+  let refine_casted ?(unsafe = false) f = Goal.enter begin fun gl ->
     let concl = Goal.concl gl in
     let env = Goal.env gl in
     let f h = let (h, c) = f h in with_type h env c concl in
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
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