Skip to content

update Iris for later credits

Ralf Jung requested to merge ralf/iris into master

Should help with the nightly build failures. Unfortunately I cannot easily test this locally since the project does not seem to work with ProofGeneral out-of-the-box

Error: Cannot find a physical path bound to logical path type with prefix refinedc.typing.

Note sure what that is about. I see some _build things in _CoqProject. Maybe dune stuff? Anyway something that breaks the workflow I have been using for 10 years... so let's just see what CI says. ;)

(make builddep insists on installing cerberus which I don't want to do since I just want to change some Coq files.)

Merge request reports