Rename seal lemmas from `_eq` to `_unseal` and make sealing stuff `Local`.

As discussed in iris!778 (comment 80612)

I renamed them into _seal_eq to be consistent with the projection of the seal record.

What's a bit odd though, since what they are doing is unsealing? seal_eq is called that because it is about @seal _ = _. But nclose_seal_eq hides the @seal behind a Definition so I don't think this still makes sense.

FWIW just nclose_unseal would be a good name IMO, without _eq -- stating the fact that this is an equality seems somewhat redundant.

I'm fine with just unseal.

How shall we call the tuples with unseal lemmas:

Definition unseal_eqs :=
  (uPred_pure_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq,
  uPred_exist_eq, uPred_internal_eq_eq, uPred_sep_eq, uPred_wand_eq,
  uPred_plainly_eq, uPred_persistently_eq, uPred_later_eq, uPred_ownM_eq,
  uPred_cmra_valid_eq, @uPred_bupd_eq).

If we drop _eq from the lemma names, _eqs no longer makes much sense. Maybe, since it's in a module, just unseal is OK?

added 3 commits

• 99c9226f...b7a5fed7 - 2 commits from branch master
• 7f028b22 - Rename seal lemmas from `_eq` to `_unseal` and make sealing stuff `Local`.

Compare with previous version

changed title from Rename seal lemmas from _eq and _seal{-_eq-} and make sealing stuff Local. to Rename seal lemmas from _eq to _{+un+}seal and make sealing stuff Local.

changed the description

added 1 commit

• bbd052a2 - Hide `_unseal` in results of `Search`.

Compare with previous version

I now also added the Add Search Blacklist for _unseal.

mentioned in merge request iris!793 (merged)

LGTM.

resolved all threads

What's our policy w.r.t. a CHANGELOG here?

These are internal definitions, so nobody should depend on them. However, there is at least one reverse dependency (= Iris) that breaks the abstraction, and other's Iris forks might do that too.

added 1 commit

• 27c34097 - CHANGELOG.

Compare with previous version

added 8 commits

• 27c34097...53c9d7f7 - 5 commits from branch master
• 85d5291f - Rename seal lemmas from `_eq` to `_unseal` and make sealing stuff `Local`.
• c215b6cc - Hide `_unseal` in results of `Search`.
• 458a3fa8 - CHANGELOG.

Compare with previous version

resolved all threads

enabled an automatic merge when the pipeline for 458a3fa8 succeeds

Merging.

@iris-users

• Rename "unsealing" lemmas from _eq to _unseal. This affects ndot_eq and nclose_eq. These unsealing lemmas are internal, so in principle you should not rely on them.

merged

mentioned in commit ebb89887