Commits · d41f8ad5c6283c6efb8ce5ea10a1b63535f02b51 · Yixuan Chen / Iris

Jan 25, 2021
- Fix CHANGELOG. · d41f8ad5
  Robbert Krebbers authored 4 years ago
  
  d41f8ad5
- Merge branch 'robbert/removeT' into 'master' · 21b7ffa1
  Robbert Krebbers authored 4 years ago
  
  Rename `ofeT`→`ofe`, `cmraT`→`cmra`, and `ucmraT`→`ucmra`. See merge request iris/iris!623
  21b7ffa1
- Merge branch 'ralf/mono-nat' into 'master' · 6451b77c
  Ralf Jung authored 4 years ago
  
  add mono_nat_auth_lb See merge request iris/iris!605
  6451b77c
Jan 23, 2021
- Fix. · 7bee0997
  Robbert Krebbers authored 4 years ago
  
  7bee0997
- Bump std++. · 130a32a2
  Robbert Krebbers authored 4 years ago
  
  130a32a2
Jan 20, 2021
- update dependencies · 7b8a6255
  Ralf Jung authored 4 years ago
  
  7b8a6255
- While we are at it, also update cFunctor → oFunctor in docs. · 402819c4
  Robbert Krebbers authored 4 years ago
  
  402819c4
- Also update docs. · a762d183
  Robbert Krebbers authored 4 years ago
  
  a762d183
Jan 19, 2021
- Rename `ofeT`→`ofe`, `cmraT`→`cmra`, and `ucmraT`→`ucmra`. · cc9470e0
  Robbert Krebbers authored 4 years ago
  
  cc9470e0
- update dependencies · eb8123ac
  Ralf Jung authored 4 years ago
  
  eb8123ac
- reject warnings on Coq 8.13 · ccc5ddf9
  Ralf Jung authored 4 years ago
  
  ccc5ddf9
Jan 17, 2021
- Bump std++. · 37945115
  Robbert Krebbers authored 4 years ago
  
  37945115
Jan 15, 2021
- test on Coq 8.13.0 · 3a636365
  Ralf Jung authored 4 years ago
  
  3a636365
- Merge branch 'ralf/big_opS' into 'master' · cc985ac8
  Robbert Krebbers authored 4 years ago
  
  add some big_opS lemmas See merge request !619
  cc985ac8
- make use of new std++ lemmas · a0ee21d2
  Ralf Jung authored 4 years ago
  
  a0ee21d2
- shorter proof by Robbert · cac67ba3
  Ralf Jung authored 4 years ago
  
  cac67ba3
- address review feedback · 42981d63
  Ralf Jung authored 4 years ago
  
  42981d63
- Apply 2 suggestion(s) to 2 file(s) · 2a444b23
  Ralf Jung authored 4 years ago
  
  2a444b23
- add some big_opS lemmas · a42a3570
  Ralf Jung authored 4 years ago
  
  a42a3570
- update dependencies · 0a8c2c18
  Ralf Jung authored 4 years ago
  
  0a8c2c18
- Merge branch 'ralf/cmra-op-discrete' into 'master' · afe06025
  Robbert Krebbers authored 4 years ago
  
  strengthen cmra_op_discrete See merge request !618
  afe06025
- changelog · c9d861f5
  Ralf Jung authored 4 years ago
  
  c9d861f5
- strengthen cmra_op_discrete · 08899f71
  Ralf Jung authored 4 years ago
  
  08899f71
Jan 14, 2021
- Merge branch 'ralf/csum_valid' into 'master' · 6ed0574d
  Robbert Krebbers authored 4 years ago
  
  add Cinl_valid, Cinr_valid See merge request !621
  6ed0574d
- add Cinl_valid, Cinr_valid · 3de1a0e8
  Ralf Jung authored 4 years ago
  
  3de1a0e8
Jan 13, 2021
- update dependencies · 086b3519
  Ralf Jung authored 4 years ago
  
  086b3519
- update dependencies · 049947a6
  Ralf Jung authored 4 years ago
  
  049947a6
- fix 8.11 reference files · eb994f18
  Ralf Jung authored 4 years ago
  
  eb994f18
- normalize 'subgoal' to 'goal' to account for Coq output change · 40ab3fea
  Ralf Jung authored 4 years ago
  
  40ab3fea
Jan 12, 2021
- Merge branch 'ralf/preg' into 'master' · bbaf3eaf
  Ralf Jung authored 4 years ago
  
  reuse PreG class in G class where possible See merge request !617
  bbaf3eaf
- apply reveiw feedback · 43853fc3
  Ralf Jung authored 4 years ago
  
  43853fc3
- reuse PreG class in G class where possible · bf2b810d
  Ralf Jung authored 4 years ago
  
  bf2b810d
Jan 08, 2021
- Bump std++. · 51cc75f3
  Robbert Krebbers authored 4 years ago
  
  51cc75f3
Jan 07, 2021
- Merge branch 'ralf/gen-heap-names' into 'master' · 8084db97
  Ralf Jung authored 4 years ago
  
  gen_heap: expose that inG identities are preserved See merge request !585
  8084db97
- explain what gen_heap_init_names is for · 3a7c26b0
  Ralf Jung authored 4 years ago
  
  3a7c26b0
- adjust docs for new PreG pattern · 339e9d14
  Ralf Jung authored 4 years ago
  
  339e9d14
- embed gen_heapPreG into gen_heapG · ea832a21
  Ralf Jung authored 4 years ago
  
  ea832a21
- gen_heap: expose that inG identities are preserved · cbb55ae0
  Ralf Jung authored 4 years ago
  
  cbb55ae0
- ensure that all Instance/Argument/Hint are qualified · a0e020ca
  Ralf Jung authored 4 years ago
  
  a0e020ca
- also add Local/Global to Arguments · 79a11082
  Ralf Jung authored 4 years ago
  
  79a11082