diff options
| author | Matthieu Sozeau | 2016-03-25 16:46:50 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-03-25 16:55:06 +0100 |
| commit | 7e7b5684d8f8066b90fca3395104af7241b8aed6 (patch) | |
| tree | 2d5f220f65eee3cca3a856bf823103d07e8aefc3 /proofs | |
| parent | 25c6356326773ac56380b81de6f58d15caae8680 (diff) | |
Univs: fix get_current_context (bug #4603, part I)
Return an evar_map with the right universes, when there are no focused
subgoals or the proof is finished.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index b635cc9632..2f5c1d1c2b 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -85,7 +85,8 @@ let get_current_goal_context () = with NoSuchGoal -> (* spiwack: returning empty evar_map, since if there is no goal, under focus, there is no accessible evar either *) - (Evd.empty, Global.env ()) + let env = Global.env () in + (Evd.from_env env, env) let current_proof_statement () = match Proof_global.V82.get_current_initial_conclusions () with |