From c215b6cc57098f4c2abd6ce6375f0795fc7a2dcb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 12 May 2022 14:17:21 +0200
Subject: [PATCH] Hide `_unseal` in results of `Search`.

---
 theories/base.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/theories/base.v b/theories/base.v
index 010b34e6..a09cd676 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -46,8 +46,10 @@ introduces all variables and gives them fresh names. As such, it becomes
 impossible to refer to hypotheses in a robust way. *)
 Obligation Tactic := idtac.
 
-(** 3. Hide obligations from the results of the [Search] commands. *)
+(** 3. Hide obligations and unsealing lemmas from the results of the [Search]
+commands. *)
 Add Search Blacklist "_obligation_".
+Add Search Blacklist "_unseal".
 
 (** * Sealing off definitions *)
 Section seal.
-- 
GitLab