4 files changed, 8 insertions, 11 deletions
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)