Skip to content

Rename `ofeT`→`ofe`, `cmraT`→`cmra`, and `ucmraT`→`ucmra`.

Robbert Krebbers requested to merge robbert/removeT into master

The T suffix are a result of some very old experiments, when I had both a bundled and unbundled version of the algebraic structures. This is long gone, and did not even make it into Iris 2.0.

The T suffix is rather confusing, and people often ask me to explain why it's there, and I do not have a good answer. Note that the bi structure does not have a T suffix either.

This MR will probably break all Iris developments in existence, but it's trivial to fix: just run a sed script.

Merge request reports