From 55dfa688b85aa7c915d0e8db414d1f9a7cf9928c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Tue, 10 Sep 2024 22:57:57 -0700
Subject: [PATCH] Sealed: mark seal/unseal as coercions

---
 ulib/FStar.Sealed.fsti         | 1 +
 ulib/FStar.Tactics.Unseal.fsti | 1 +
 2 files changed, 2 insertions(+)

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