From d929838be77e30db04cd91201542bb52ed3ff7fd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 25 Jun 2019 20:57:50 +0200
Subject: Similar purity invariants in the kernel.

---
 tactics/declare.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/declare.ml b/tactics/declare.ml
index 7ad86baa8d..b8ba62a5e5 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -289,7 +289,7 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind
   | None -> Cmap.empty
   | Some r -> Cmap.singleton kn r
   in
-  let eff = { Evd.seff_private = eff; Evd.seff_roles; } in
+  let eff = { Evd.seff_private = eff.Entries.seff_wrap; Evd.seff_roles; } in
   kn, eff
 
 (** Declaration of section variables and local definitions *)
-- 
cgit v1.2.3