I think the notation for embedded Coq assertions and for plainly should include an affinely modality -- that way, one can just always use * and -* even when working in linear Iris.
*
-*
