Update Iris, fix some cases in rebor, tweak some proofs.
In particular, I started changing some lemmas in borrow.v to not unfold everything right away. Unfolding everything right away yields very big goals that do not fit in one screen and makes stuff slow.
Showing
- iris 1 addition, 1 deletioniris
- theories/lang/heap.v 2 additions, 3 deletionstheories/lang/heap.v
- theories/lang/proofmode.v 10 additions, 11 deletionstheories/lang/proofmode.v
- theories/lifetime/accessors.v 0 additions, 1 deletiontheories/lifetime/accessors.v
- theories/lifetime/borrow.v 60 additions, 47 deletionstheories/lifetime/borrow.v
- theories/lifetime/creation.v 2 additions, 2 deletionstheories/lifetime/creation.v
- theories/lifetime/derived.v 2 additions, 3 deletionstheories/lifetime/derived.v
- theories/lifetime/rebor.v 28 additions, 29 deletionstheories/lifetime/rebor.v
Loading
Please register or sign in to comment