diff options
Diffstat (limited to 'proofs/proof_global.ml')
| -rw-r--r-- | proofs/proof_global.ml | 11 |
1 files changed, 6 insertions, 5 deletions
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) |