diff --git a/theories/base.v b/theories/base.v
index 010b34e610c46dc39aae5451433c6051ebd28581..a09cd676ff7b92e32dd709ab3e11fa3df9047aba 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.