From 46c0b7ab3653a6f1ef4b40466c2dd130d09136cb Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 11 Jun 2020 18:51:34 +0200
Subject: Move given_up goals to evar_map

---
 vernac/vernacentries.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'vernac')

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 =
-- 
cgit v1.2.3