diff --git a/ulib/FStar.Sealed.fsti b/ulib/FStar.Sealed.fsti
index c14905a9013..6247eab3cab 100644
--- a/ulib/FStar.Sealed.fsti
+++ b/ulib/FStar.Sealed.fsti
@@ -44,6 +44,7 @@ val sealed_singl (#a:Type) (x y : sealed a)
   : Lemma (x == y)
 
 (* Sealing a value hides it from the logical fragment of F* *)
+[@@coercion]
 val seal (#a : Type u#aa) (x:a) : Tot (sealed a)
 
 val map_seal (#a : Type u#aa) (#b : Type u#bb) (s : sealed a) (f : a -> Tot b) : Tot (sealed b)
diff --git a/ulib/FStar.Tactics.Unseal.fsti b/ulib/FStar.Tactics.Unseal.fsti
index b2ee8515f9e..557b993191f 100644
--- a/ulib/FStar.Tactics.Unseal.fsti
+++ b/ulib/FStar.Tactics.Unseal.fsti
@@ -22,4 +22,5 @@ open FStar.Sealed
 open FStar.Tactics.Effect
 
 (** Observe a sealed value. See Sealed.seal too. *)
+[@@coercion]
 val unseal : #a:Type -> sealed a -> Tac a