diff options
| author | Emilio Jesus Gallego Arias | 2019-07-01 04:00:11 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-11 18:19:12 +0200 |
| commit | 2576fee1798b753161a730244c8d4d701e8a4641 (patch) | |
| tree | e07fa6b7e015b08565fd73c9f36c4dcf8cc2cfed /proofs/pfedit.ml | |
| parent | efe7108a0ae32faeb674cc5d97e6fa955a1dccd8 (diff) | |
[proof] Minor cleanup in proof.ml
Diffstat (limited to 'proofs/pfedit.ml')
| -rw-r--r-- | proofs/pfedit.ml | 4 |
1 files changed, 2 insertions, 2 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 |