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

---
 toplevel/coqloop.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 79de3c86b6..9917ae0f01 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -324,12 +324,12 @@ let loop_flush_all () =
 let pequal cmp1 cmp2 (a1,a2) (b1,b2) = cmp1 a1 b1 && cmp2 a2 b2
 let evleq e1 e2 = CList.equal Evar.equal e1 e2
 let cproof p1 p2 =
-  let Proof.{goals=a1;stack=a2;shelf=a3;given_up=a4} = Proof.data p1 in
-  let Proof.{goals=b1;stack=b2;shelf=b3;given_up=b4} = Proof.data p2 in
+  let Proof.{goals=a1;stack=a2;shelf=a3;sigma=sigma1} = Proof.data p1 in
+  let Proof.{goals=b1;stack=b2;shelf=b3;sigma=sigma2} = Proof.data p2 in
   evleq a1 b1 &&
   CList.equal (pequal evleq evleq) a2 b2 &&
   CList.equal Evar.equal a3 b3 &&
-  CList.equal Evar.equal a4 b4
+  Evar.Set.equal (Evd.given_up sigma1) (Evd.given_up sigma2)
 
 let drop_last_doc = ref None
 
-- 
cgit v1.2.3