diff --git a/stdpp/base.v b/stdpp/base.v
index 386841006a6db7522f0dab848d7ed68d5ee9cbe6..45e5a5f87df22c93a78b4f764e819957ba8c136a 100644
--- a/stdpp/base.v
+++ b/stdpp/base.v
@@ -52,10 +52,8 @@ Add Search Blacklist "_obligation_".
 Add Search Blacklist "_unseal".
 
 (** * Sealing off definitions *)
-Section seal.
-  Local Set Primitive Projections.
-  Record seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }.
-End seal.
+#[projections(primitive=yes)]
+Record seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }.
 Global Arguments unseal {_ _} _ : assert.
 Global Arguments seal_eq {_ _} _ : assert.