Make `unseal` TC opaque

This had a very slight positive impact on our development. But we don't have a lot of things sealed this way so the impact might be bigger in other developments.

We just recently had a bug that was resolved by not making something both sealed an TC opaque: https://github.com/coq/coq/issues/17720. So this change might be risky.

resolved all threads

added 1 commit

• b36b4c3a - Use `Global` instead of `#[global]` for consistency

Compare with previous version

I am happy to merge this if CI gives no performance regressions.

That said, I hope unseal will "soon" be replaced by Elpi's locker. See the discussion in iris#528

We can't time std++ changes, so whether there are perf regressions will only become clear after merging.

What do we want to do here?

Even though this MR might become obsolete, I am fine with merging and reverting if it causes regressions.

I've done baseline timings with current Iris, so let's merge this and see if anything changes.

merged

mentioned in commit 36874919

This breaks the Iris build. I am going to revert.

File "./iris/base_logic/lib/ghost_var.v", line 119, characters 9-32:
Error: Could not fill dependent hole in "apply"

File "./iris/base_logic/lib/gen_heap.v", line 194, characters 9-32:
Error: Could not fill dependent hole in "apply"

mentioned in commit 79877aad

mentioned in merge request !504 (merged)