diff options
| author | Maxime Dénès | 2020-06-11 18:51:34 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-08-26 16:38:34 +0200 |
| commit | 46c0b7ab3653a6f1ef4b40466c2dd130d09136cb (patch) | |
| tree | b6937b47990e5f76b3f9a5b0fc8999754334ce26 /vernac | |
| parent | 4e59a68fd6f2cd3cdf936c10cdbfeb46fc22ca95 (diff) | |
Move given_up goals to evar_map
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 548f59559a..4e08a40d6b 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -112,7 +112,8 @@ let show_proof ~pstate = let show_top_evars ~proof = (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *) - let Proof.{goals;shelf;given_up;sigma} = Proof.data proof in + let Proof.{goals;shelf;sigma} = Proof.data proof in + let given_up = Evar.Set.elements @@ Evd.given_up sigma in pr_evars_int sigma ~shelf ~given_up 1 (Evd.undefined_map sigma) let show_universes ~proof = |