Comments Ralf.

iris/base_logic/bi.v

@@ -291,7 +291,7 @@ Section restate.
     upred.uPred_ownM_unseal, upred.uPred_cmra_valid_unseal, @uPred_bupd_unseal).
 End restate.
 
-(** The final unseal tactic that also unfolds the BI layer. This is used by
-[base_logic.algebra] and [base_logic.bupd_alt]. *)
+(** A tactic for rewriting with the above lemmas. Unfolds [uPred] goals that use
+the BI layer. This is used by [base_logic.algebra] and [base_logic.bupd_alt]. *)
 Ltac unseal := rewrite !uPred_unseal /=.
 End uPred.

iris/bi/monpred.v

@@ -545,10 +545,11 @@ Section instances.
   (** And finally the proper [unseal] tactic (which we also redefine outside
   of the section since Ltac definitions do not outlive a section). *)
   Local Definition monPred_unseal :=
-    (monPred_unseal_bi, @monPred_embed_unseal, @monPred_internal_eq_unseal,
-    @monPred_bupd_unseal, @monPred_fupd_unseal, @monPred_plainly_unseal,
+    (monPred_unseal_bi,
     @monPred_defs.monPred_objectively_unseal,
     @monPred_defs.monPred_subjectively_unseal,
+    @monPred_embed_unseal, @monPred_internal_eq_unseal,
+    @monPred_bupd_unseal, @monPred_fupd_unseal, @monPred_plainly_unseal,
     @monPred_defs.monPred_in_unseal).
   Ltac unseal := rewrite !monPred_unseal /=.