[proof] Minor cleanup in proof.ml

6 files changed, 14 insertions, 16 deletions

diff --git a/printing/printer.ml b/printing/printer.ml
index 97b3233d12..ec1b9b8e49 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -825,9 +825,9 @@ let pr_nth_open_subgoal ~proof n =
 
 let pr_goal_by_id ~proof id =
   try
-    Proof.in_proof proof (fun sigma ->
-      let g = Evd.evar_key id sigma in
-      pr_selected_subgoal (pr_id id) sigma g)
+    let { Proof.sigma } = Proof.data proof in
+    let g = Evd.evar_key id sigma in
+    pr_selected_subgoal (pr_id id) sigma g
   with Not_found -> user_err Pp.(str "No such goal.")
 
 (** print a goal identified by the goal id as it appears in -emacs mode.
@@ -843,7 +843,8 @@ let pr_goal_emacs ~proof gid sid =
           ++ pr_goal gs)
     in
     try
-      Proof.in_proof proof (fun sigma -> pr {it=(Evar.unsafe_of_int gid);sigma=sigma;})
+      let { Proof.sigma } = Proof.data proof in
+      pr { it = Evar.unsafe_of_int gid ; sigma }
     with Not_found -> user_err Pp.(str "No such goal.")
 
 (* Printer function for sets of Assumptions.assumptions.
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index ed60b8274a..99a254652c 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -61,8 +61,8 @@ let get_current_context pf =
   with
   | NoSuchGoal ->
     (* No more focused goals *)
-    let evd = Proof.in_proof p (fun x -> x) in
-    evd, Global.env ()
+    let { Proof.sigma } = Proof.data p in
+    sigma, Global.env ()
 
 let solve ?with_end_tac gi info_lvl tac pr =
     let tac = match with_end_tac with
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 9f2c90c375..5f07cc1acc 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -398,8 +398,6 @@ let run_tactic env tac pr =
 
 (*** Commands ***)
 
-let in_proof p k = k (Proofview.return p.proofview)
-
 (* Remove all the goals from the shelf and adds them at the end of the
    focused goals. *)
 let unshelve p =
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 7e535a258c..9973df492d 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -176,8 +176,6 @@ val maximal_unfocus : 'a focus_kind -> t -> t
 
 (*** Commands ***)
 
-val in_proof : t -> (Evd.evar_map -> 'a) -> 'a
-
 (* Remove all the goals from the shelf and adds them at the end of the
    focused goals. *)
 val unshelve : t -> t
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index ab8d87c100..851a3d1135 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -177,7 +177,8 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
      have existential variables in the initial types of goals, we need to
      normalise them for the kernel. *)
   let subst_evar k =
-    Proof.in_proof proof (fun m -> Evd.existential_opt_value0 m k) in
+    let { Proof.sigma } = Proof.data proof in
+    Evd.existential_opt_value0 sigma k in
   let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar
     (UState.subst universes) in
 
@@ -307,7 +308,7 @@ let close_proof ~opaque ~keep_body_ucst_separate fix_exn ps =
 
 let update_global_env =
   map_proof (fun p ->
-      Proof.in_proof p (fun sigma ->
-          let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in
-          let p,(status,info),_ = Proof.run_tactic (Global.env ()) tac p in
-          p))
+      let { Proof.sigma } = Proof.data p in
+      let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in
+      let p, (status,info), _ = Proof.run_tactic (Global.env ()) tac p in
+      p)
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index 3b8fc58c6f..17004bb012 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -763,7 +763,7 @@ let perform_eval ~pstate e =
   | Goal_select.SelectAlreadyFocused -> assert false (* TODO **)
   in
   let (proof, _, ans) = Proof.run_tactic (Global.env ()) v proof in
-  let sigma = Proof.in_proof proof (fun sigma -> sigma) in
+  let { Proof.sigma } = Proof.data proof in
   let name = int_name () in
   Feedback.msg_notice (str "- : " ++ pr_glbtype name (snd ty)
     ++ spc () ++  str "=" ++ spc () ++