Skip to content

fix Coq 8.18 deprecation warnings

Ralf Jung requested to merge jung/iris:ralf/coq-8.18 into master

Coq started warning about Let. ... Qed.. And it is right, this makes little sense -- Let means "make this completely transparent after the section"; Qed means "make this opaque".

So let's either make these non-Qed when the proofs are completely trivial, or non-Let when the proofs are complicated enough that we want them to be opaque.

Merge request reports