improve view shift and Hoare triple printing (163e26ee) · Commits · Gaëtan Gilbert / Iris · GitLab

Skip to content

GitLab

Explore

Sign in

Primary navigation

Project

Iris
- Activity
- Members
- Labels
- Issues
- Issue boards
- Milestones
- Wiki
- Terraform modules
- Service Desk

Snippets Groups Projects

163e26ee

Commit 163e26ee authored 3 years ago by Ralf Jung

Downloads
- Patches
- Plain Diff

improve view shift and Hoare triple printing

to avoid bad regressions, some other notations also ha to be tweaked

parent 28b051a0

No related branches found

No related tags found

No related merge requests found

Changes 13

Hide whitespace changes

Inline Side-by-side

Showing

iris/base_logic/lib/fancy_updates_from_vs.v 1 addition, 3 deletions

iris/base_logic/lib/fancy_updates_from_vs.v
iris/bi/lib/counterexamples.v 1 addition, 2 deletions

iris/bi/lib/counterexamples.v
iris/bi/notation.v 16 additions, 16 deletions

iris/bi/notation.v
iris/bi/weakestpre.v 20 additions, 20 deletions

iris/bi/weakestpre.v
iris/program_logic/atomic.v 4 additions, 4 deletions

iris/program_logic/atomic.v
iris/proofmode/notation.v 4 additions, 4 deletions

iris/proofmode/notation.v
tests/atomic.ref 19 additions, 21 deletions

tests/atomic.ref
tests/heap_lang_printing.ref 20 additions, 30 deletions

tests/heap_lang_printing.ref
tests/one_shot.ref 9 additions, 9 deletions

tests/one_shot.ref
tests/one_shot_once.ref 10 additions, 10 deletions

tests/one_shot_once.ref
tests/proofmode.ref 18 additions, 18 deletions

tests/proofmode.ref
tests/proofmode_ascii.ref 2 additions, 2 deletions

tests/proofmode_ascii.ref
tests/proofmode_iris.ref 4 additions, 4 deletions

tests/proofmode_iris.ref

with 128 additions and 143 deletions

Loading

0% Loading or .

You are about to add 0 people to the discussion. Proceed with caution.

Finish editing this message first!

Please register or sign in to comment