only locally make uPred_holds a coercion

uPred_holds being a coercion globally breaks the uPred abstraction. So only make it a coercion in modules that go into the model anyway.

While at it, I did the same for siProp.

added 1 commit

• a0818a08 - only locally make siProp_holds a coercion

Compare with previous version

changed the description

LGTM, modulo nit about comment.

added 2 commits

• 48068213 - only locally make uPred_holds a coercion
• 2c1dd026 - only locally make siProp_holds a coercion

Compare with previous version

Looks good to me.

resolved all threads

merged

mentioned in commit c4ea27fb

@iris-users this is a breaking change if you were relying on the uPred_holds coercion (which should be rare, it only happens when you go down into the model of Iris).