From 39c4f9030f3aefdb7581aa02dd4b0c0d1ef89ee5 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 26 Mar 2020 19:53:51 -0400
Subject: [sideeff] Don't use polymorphic equality to check for empty
 side-effects

---
 vernac/declareDef.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/declareDef.ml')

diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 1607771598..601e7e060c 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -171,7 +171,7 @@ let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma =
   let ce = definition_entry ?opaque ?inline ?types ~univs body in
   let env = Global.env () in
   let (c,ctx), sideff = Future.force ce.Declare.proof_entry_body in
-  assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private);
+  assert(Safe_typing.is_empty_private_constants sideff.Evd.seff_private);
   assert(Univ.ContextSet.is_empty ctx);
   RetrieveObl.check_evars env sigma;
   let c = EConstr.of_constr c in
-- 
cgit v1.2.3