Iris merge requestshttps://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests2023-08-28T12:02:37Zhttps://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/972Draft: experiment: use coq's ability to infer more canonical structures2023-08-28T12:02:37ZRalf Jungjung@mpi-sws.orgDraft: experiment: use coq's ability to infer more canonical structuresI wonder if we should recommend this style, once all Coq versions we support can handle it. It is certainly much nicer, we could entirely hide these `R`/`UR` terms from users. Unfortunately in one case already in this repo, it requires m...I wonder if we should recommend this style, once all Coq versions we support can handle it. It is certainly much nicer, we could entirely hide these `R`/`UR` terms from users. Unfortunately in one case already in this repo, it requires more type annotations. I don't understand why Coq cannot infer that any more.https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/933Make bi fields non-canonical2023-10-13T14:37:45ZPaolo G. GiarrussoMake bi fields non-canonicalSuggested by @janno .Suggested by @janno .