Forked from
Iris / Iris
Source project has a limited visibility.
-
Robbert Krebbers authored
- Make `flöb_pre` and `flöb` local to the proof. - The metavariables `Ψ` are used for predicates, so use a `Q` here.
Robbert Krebbers authored- Make `flöb_pre` and `flöb` local to the proof. - The metavariables `Ψ` are used for predicates, so use a `Q` here.
