diff --git a/theories/base.v b/theories/base.v
index cf4781b8f2558ac3c90eefc4b06f1c0a343cf42b..48a5fd0f81ef00f777e19cf26ae13b1ad63f78ec 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -18,11 +18,12 @@ Obligation Tactic := idtac.
 Add Search Blacklist "_obligation_".
 
 (** Sealing off definitions *)
-Set Primitive Projections.
-Record seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }.
-Arguments unseal {_ _} _ : assert.
-Arguments seal_eq {_ _} _ : assert.
-Unset Primitive Projections.
+Section seal.
+  Local Set Primitive Projections.
+  Record seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }.
+  Arguments unseal {_ _} _ : assert.
+  Arguments seal_eq {_ _} _ : assert.
+End seal.
 
 (** Typeclass opaque definitions *)
 (* The constant [tc_opaque] is used to make definitions opaque for just type