Renaming Goal.enter field into s_enter.

2 files changed, 12 insertions, 12 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index da9c4da9f9..7edbef57b4 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -974,8 +974,8 @@ module Goal = struct
     end
     end
 
-  type 'a enter =
-    { enter : 'r. 'a t -> 'r Sigma.t -> (unit tactic, 'r) Sigma.sigma }
+  type 'a s_enter =
+    { s_enter : 'r. 'a t -> 'r Sigma.t -> (unit tactic, 'r) Sigma.sigma }
 
   let s_enter f =
     InfoL.tag (Info.Dispatch) begin
@@ -985,7 +985,7 @@ module Goal = struct
       try
         let gl = gmake env sigma goal in
         let sigma = Sigma.Unsafe.of_evar_map sigma in
-        let Sigma (tac, sigma, _) = f.enter gl sigma in
+        let Sigma (tac, sigma, _) = f.s_enter gl sigma in
         let sigma = Sigma.to_evar_map sigma in
         tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) tac)
       with e when catchable_exception e ->
@@ -1002,7 +1002,7 @@ module Goal = struct
       try
         let (gl, sigma) = nf_gmake env sigma goal in
         let sigma = Sigma.Unsafe.of_evar_map sigma in
-        let Sigma (tac, sigma, _) = f.enter gl sigma in
+        let Sigma (tac, sigma, _) = f.s_enter gl sigma in
         let sigma = Sigma.to_evar_map sigma in
         tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) tac)
       with e when catchable_exception e ->
@@ -1254,6 +1254,6 @@ module Notations = struct
   let (>>=) = tclBIND
   let (<*>) = tclTHEN
   let (<+>) t1 t2 = tclOR t1 (fun _ -> t2)
-  type 'a enter = 'a Goal.enter =
-    { enter : 'r. 'a Goal.t -> 'r Sigma.t -> (unit tactic, 'r) Sigma.sigma }
+  type 'a s_enter = 'a Goal.s_enter =
+    { s_enter : 'r. 'a Goal.t -> 'r Sigma.t -> (unit tactic, 'r) Sigma.sigma }
 end
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index b565589eb7..a94610af47 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -454,16 +454,16 @@ module Goal : sig
   (** Like {!nf_enter}, but does not normalize the goal beforehand. *)
   val enter : ([ `LZ ] t -> unit tactic) -> unit tactic
 
-  type 'a enter =
-    { enter : 'r. 'a t -> 'r Sigma.t -> (unit tactic, 'r) Sigma.sigma }
+  type 'a s_enter =
+    { s_enter : 'r. 'a t -> 'r Sigma.t -> (unit tactic, 'r) Sigma.sigma }
 
   (** A variant of {!enter} allows to work with a monotonic state. The evarmap
       returned by the argument is put back into the current state before firing
       the returned tactic. *)
-  val s_enter : [ `LZ ] enter -> unit tactic
+  val s_enter : [ `LZ ] s_enter -> unit tactic
 
   (** Like {!s_enter}, but normalizes the goal beforehand. *)
-  val nf_s_enter : [ `NF ] enter -> unit tactic
+  val nf_s_enter : [ `NF ] s_enter -> unit tactic
 
   (** Recover the list of current goals under focus, without evar-normalization *)
   val goals : [ `LZ ] t tactic list tactic
@@ -592,6 +592,6 @@ module Notations : sig
   (** {!tclOR}: [t1+t2] = [tclOR t1 (fun _ -> t2)]. *)
   val (<+>) : 'a tactic -> 'a tactic -> 'a tactic
 
-  type 'a enter = 'a Goal.enter =
-    { enter : 'r. 'a Goal.t -> 'r Sigma.t -> (unit tactic, 'r) Sigma.sigma }
+  type 'a s_enter = 'a Goal.s_enter =
+    { s_enter : 'r. 'a Goal.t -> 'r Sigma.t -> (unit tactic, 'r) Sigma.sigma }
 end