Commits · b3c142a2ca5188cbd27fb99fc1649d34ca57bf7f · Pierre Roux / Iris

Sep 05, 2021
- make binary wand/view shift connectives 'block' formated · b3c142a2
  Ralf Jung authored 3 years ago
  
  b3c142a2
Jul 29, 2021
- add some missing test name markers to proofmode_iris · bfccb2a2
  Ralf Jung authored 3 years ago
  
  bfccb2a2
- fix atomic update trailing spaces · 13063825
  Ralf Jung authored 3 years ago
  
  13063825
- defensive formatting: put a box around the proofmode context · 42d90c3d
  Ralf Jung authored 3 years ago
  
  suggested by Huge Herbelin
  42d90c3d
Jul 28, 2021
- make logatom printing consistent with new WP/Texan Triple printing · ee8bef79
  Ralf Jung authored 3 years ago
  
  ee8bef79
- improve view shift and Hoare triple printing · 163e26ee
  Ralf Jung authored 3 years ago
  
  to avoid bad regressions, some other notations also ha to be tweaked
  163e26ee
- improve WP printing · 28b051a0
  Ralf Jung authored 3 years ago
  
  28b051a0
Jul 27, 2021
- add some more challenging printing tests · 4f711829
  Ralf Jung authored 3 years ago
  
  4f711829
Jul 26, 2021
- move heap_lang printing tests to separate file · 6e239f95
  Ralf Jung authored 3 years ago
  
  6e239f95
- import options in tests · 0872908e
  Ralf Jung authored 3 years ago
  
  0872908e
Jul 25, 2021
- add NonExpansive3, NonExpansive4 · 38881ccf
  Ralf Jung authored 3 years ago
  
  38881ccf
- Similar tests for `curry`. · 7607c53e
  Robbert Krebbers authored 3 years ago
  
  7607c53e
- Tests for non-expansive of uncurry. · fdf4deed
  Robbert Krebbers authored 3 years ago
  
  fdf4deed
Jul 19, 2021
- avoid line-breaking within the mask part of AU/AACC · 859fbccb
  Ralf Jung authored 3 years ago
  
  859fbccb
Jun 19, 2021

Include workaround for Coq bug #14441, and drop now-failing test for that Coq
bug.

Verified

5f5c02af

Jun 18, 2021
- use 'MIEnvTransform IntoLaterable' for iAuIntro · 0dfb3b34
  Ralf Jung authored 3 years ago
  
  0dfb3b34
- add test for make_laterable iModIntro · 6edb48ba
  Ralf Jung authored 3 years ago
  
  6edb48ba
- don't test 'Hint Mode Equiv !'; wait for Coq fix instead · bd9d16c9
  Ralf Jung authored 3 years ago
  
  bd9d16c9
- Revise comments on tests · a02c29ac
  Paolo G. Giarrusso authored 3 years ago
  
  Verified
  
  a02c29ac
- Add suggested test · ac3ddfda
  Paolo G. Giarrusso authored 3 years ago
  
  Verified
  
  ac3ddfda
Jun 17, 2021
- explicit coercion > type ascription · abfe8672
  Ralf Jung authored 3 years ago
  
  abfe8672
- fix tests · a8ce6616
  Ralf Jung authored 4 years ago
  
  a8ce6616
Jun 14, 2021
- Improve error messages for sel/spec/intro pat. · 52547f53
  Robbert Krebbers authored 3 years ago
  
  52547f53
- Add tests. · b470f38b
  Robbert Krebbers authored 3 years ago
  
  b470f38b
Jun 02, 2021
- update ref files · 7f0c8a58
  Ralf Jung authored 3 years ago
  
  7f0c8a58
- rename global singletons to 'GS' suffix · 1118f70f
  Ralf Jung authored 3 years ago
  
  1118f70f
May 31, 2021
- Add (non-persistent) IntoAnd & IntoForall for bupd/fupd · b2bb853f
  Paolo G. Giarrusso authored 3 years ago
  
  Verified
  
  b2bb853f
May 25, 2021
- better error for iModIntro on mask-changing update · 0e1bdaf4
  Ralf Jung authored 3 years ago
  
  0e1bdaf4
- better error when iMod fails due to mask mismatch · fd243450
  Ralf Jung authored 3 years ago
  
  fd243450
May 19, 2021
- fix tests · c1696b8d
  Simon Hudon authored 3 years ago
  
  c1696b8d
May 17, 2021
- Add test case for Xchg · 32300303
  Simon Hudon authored 3 years ago
  
  32300303
May 13, 2021
- test bi Lemma scopes · b600a5bb
  Ralf Jung authored 3 years ago
  
  b600a5bb
Apr 14, 2021
- Fix string_to_ident when ident is not fresh · 20d74b17
  Tej Chajed authored 3 years ago and Ralf Jung committed 3 years ago
  
  20d74b17
Mar 27, 2021
- remove now stale .ref files · 6415d82a
  Ralf Jung authored 4 years ago
  
  6415d82a
Mar 25, 2021
- add test for dependent nested exist · 0e7930c6
  Ralf Jung authored 4 years ago
  
  0e7930c6
Mar 24, 2021
- different approach for string_to_ident that works with name mangling · 2eb8bde0
  Ralf Jung authored 4 years ago
  
  2eb8bde0
- add more tests · 7da8952e
  Ralf Jung authored 4 years ago
  
  7da8952e
- more exist destruct test cases · 6be1cdd2
  Ralf Jung authored 4 years ago
  
  6be1cdd2
- replace iAndDestruct hack for [% %] by more general IntoExist instances · 6dc7e98a
  Ralf Jung authored 4 years ago
  
  6dc7e98a
- Apply 1 suggestion(s) to 1 file(s) · b9d25e99
  Tej Chajed authored 4 years ago and Ralf Jung committed 4 years ago
  
  b9d25e99