Sorry to bring this up again, I just think it's important to get this as right as we can, right now. ;)
This moves the global functor and dynamic composeable ownership to
base_logic. The reasoning behind this is that if someone builds another program logic in our base logic, they will likely want to re-use this, so it makes more sense to have it in base_logic than in program_logic.
The rule for stuff to be in program_logic is: It depends on the Iris' notion of a language, or on world satisfaction (i.e., on our specific way to do invariants). Thus,
saved_prop also moves to
base_logic and becomes reusable by other program logics.
(If we want, we can talk about changing this to just "anything that depends on our notion of a language". Is it conceivable that our world satisfaction is reusable?)
When we talked about this previously, Robbert raised concerns about the name
iProp. However, considering that we also have
iTactics and use
I for the
uPred_scope, I feel like the letter "i" has already leaked way beyond
program_logic, so this PR doesn't actually change anything. If you want, interpret
iProp as "internal propositions", that even makes sense. ;)