diff --git a/theories/base.v b/theories/base.v
index 92606a94b39483093fc2900afbeff5687503ae0f..e1c36a0aeb0ef85a6d46a9fe3033a8d54e423823 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -14,6 +14,13 @@ Export ListNotations.
 From Coq.Program Require Export Basics Syntax.
 Obligation Tactic := idtac.
 
+(** Sealing off definitions *)
+Set Primitive Projections.
+Record seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }.
+Arguments unseal {_ _} _.
+Arguments seal_eq {_ _} _.
+Unset Primitive Projections.
+
 (** Throughout this development we use [C_scope] for all general purpose
 notations that do not belong to a more specific scope. *)
 Delimit Scope C_scope with C.