Missing unseal tactic for siProp
Here's what I've used:
(* XXX Taken from uPred.unseal / monPred.unseal, since this logic is missing for siLogic. *) Ltac unseal_prepare := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *) unfold bi_affinely, bi_absorbingly, bi_except_0, bi_pure, bi_emp, monPred_upclosed, bi_and, bi_or, bi_impl, bi_forall, bi_exist, bi_sep, bi_wand, bi_persistently, bi_affinely, bi_later; simpl. (* Should be siProp.unseal. *) Ltac siProp_unseal := unseal_prepare; siProp_primitive.unseal.
The second part is easy, but the first not (tho it was worse before the bi-sbi merge), and deserves to be abstracted.