diff --git a/theories/base.v b/theories/base.v
index 48a5fd0f81ef00f777e19cf26ae13b1ad63f78ec..f0964e3cbf3230bc4a3b0676cad4cad3fafbab90 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -21,9 +21,9 @@ Add Search Blacklist "_obligation_".
 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.
+Arguments unseal {_ _} _ : assert.
+Arguments seal_eq {_ _} _ : assert.
 
 (** Typeclass opaque definitions *)
 (* The constant [tc_opaque] is used to make definitions opaque for just type