Commits · 11b16c7a5f6f05da49ba8a11e7de8fc8766dfba0 · Gaëtan Gilbert / Iris

Nov 18, 2022
- Merge branch 'robbert/big_op_binder' into 'master' · 11b16c7a
  Ralf Jung authored 2 years ago
  
  Use `binder` in notations for big ops See merge request iris/iris!867
  11b16c7a
Nov 17, 2022
- Document FIXME. · 0721fd0d
  Robbert Krebbers authored 2 years ago
  
  0721fd0d
- More tests. · 551085f2
  Robbert Krebbers authored 2 years ago
  
  551085f2
- Test with custom inductive. · fdfe3d31
  Robbert Krebbers authored 2 years ago
  
  fdfe3d31
- Fix for iris/iris!867 (comment 86458) · 4ace54e6
  Robbert Krebbers authored 2 years ago
  
  4ace54e6
- test Coq 8.16.0 · 30a694b8
  Ralf Jung authored 2 years ago
  
  30a694b8
- CHANGELOG. · b83e6cad
  Robbert Krebbers authored 2 years ago
  
  b83e6cad
- Some tests. · 39a49468
  Robbert Krebbers authored 2 years ago
  
  39a49468
- Use `binder` in notations for big ops. · 099b688c
  Robbert Krebbers authored 2 years ago
  
  099b688c
Nov 16, 2022
- Merge branch 'typo' into 'master' · da02a192
  Ralf Jung authored 2 years ago
  
  fix typo See merge request iris/iris!866
  da02a192
- Merge branch 'robbert/rewrite_pure_intro_pat' into 'master' · 0f15f7df
  Ralf Jung authored 2 years ago
  
  Consider intro pattern `IRewrite` (->/<-) to be intuitionistic See merge request iris/iris!856
  0f15f7df
- Consider intro pattern `IRewrite` (->/<-) to be intuitionistic · 7b3ccc15
  Robbert Krebbers authored 2 years ago and Ralf Jung committed 2 years ago
  
  7b3ccc15
- fix typo · ee61f8cd
  Armaël Guéneau authored 2 years ago
  
  ee61f8cd
- Merge branch 'robbert/no_native_compute' into 'master' · 8d8fbde9
  Ralf Jung authored 2 years ago
  
  Avoid relying on native_compute. See merge request iris/iris!865
  8d8fbde9
- Avoid relying on native_compute. · 93d9ef74
  Robbert Krebbers authored 2 years ago
  
  93d9ef74
Nov 15, 2022
- clarify that the unstable packages needs a dev version · 223b5ea8
  Ralf Jung authored 2 years ago
  
  223b5ea8
Nov 14, 2022

Merge branch 'paolo/style-end-operators' into 'master' · f156c5a4
Robbert Krebbers authored 2 years ago
```
Style: `:=` belongs to line end

See merge request iris/iris!864
```
f156c5a4

Style: `:=` belongs to line end · 8a486dbf

These are all the occurrences of `^ *:=`. `:=$` occurs ~2000 times between Iris
and stdpp.

Noticed while confirming this is the preferred stdpp/iris style.

8a486dbf

Nov 09, 2022
- Merge branch 'transitive-closure' into 'master' · c9b39944
  Robbert Krebbers authored 2 years ago
  
  Add transitive closure for bi See merge request iris/iris!862
  c9b39944
- Add transitive closure for bi · 97a7ff0c
  Simcha van Collem authored 2 years ago and Robbert Krebbers committed 2 years ago
  
  97a7ff0c
- Merge branch 'auth_update_frag_included' into 'master' · 9e4b6dfc
  Robbert Krebbers authored 2 years ago
  
  Added [cmra_update_included] lemma See merge request iris/iris!861
  9e4b6dfc
- Added [cmra_update_included] lemma · d9247945
  Jonas Kastberg authored 2 years ago
  
  d9247945
Nov 02, 2022
- update dependencies · ceba97f6
  Ralf Jung authored 2 years ago
  
  ceba97f6
Oct 31, 2022
- Merge branch 'robbert/iSpecialize_forall' into 'master' · 1e9db5bd
  Ralf Jung authored 2 years ago
  
  Better instance for `IntoWand` of `∀ _ : φ, P` Closes #492 See merge request iris/iris!860
  1e9db5bd
- Tests, the same we have for `⌜ φ ⌝ → ...`. · 8812a3a3
  Robbert Krebbers authored 2 years ago
  
  8812a3a3
- Better instance for `IntoWand` of `∀ _ : φ, P`. Fixes #799. · 25131c02
  Robbert Krebbers authored 2 years ago
  
  25131c02
Oct 28, 2022
- Merge branch 'fix_link' into 'master' · c4aeb8dd
  Ralf Jung authored 2 years ago
  
  docs/proof_guide.md: fix broken link See merge request iris/iris!859
  c4aeb8dd
- docs/proof_guide.md: fix broken link · acaaa588
  Armaël Guéneau authored 2 years ago
  
  acaaa588
- Merge branch 'heaplang-form-cleanup' into 'master' · 20047cf1
  Ralf Jung authored 2 years ago
  
  Clean up \valForm / \exprForm See merge request iris/iris!853
  20047cf1
- Clean up \valForm / \exprForm · 2a680dab
  Jonas Kastberg authored 2 years ago and Ralf Jung committed 2 years ago
  
  2a680dab
- Merge branch 'heaplang-tex-additions' into 'master' · b0618979
  Ralf Jung authored 2 years ago
  
  Changed HeapLang operator macros to support both parentheses and spaces See merge request iris/iris!852
  b0618979
- Changed HeapLang operator macros to support both parentheses and spaces · c453c97d
  Jonas Kastberg authored 2 years ago and Ralf Jung committed 2 years ago
  
  c453c97d
Oct 27, 2022
- update dependencies · e2b9bfb2
  Ralf Jung authored 2 years ago
  
  e2b9bfb2
- Merge branch 'simon/typeclass-implicit-arguments' into 'master' · f74aa92a
  Ralf Jung authored 2 years ago
  
  Disable Implicit Generalization for Typeclass Arguments See merge request iris/iris!855
  f74aa92a
- Disable Implicit Generalization for Typeclass Arguments · 334a07db
  Simon Spies authored 2 years ago and Ralf Jung committed 2 years ago
  
  334a07db
Oct 07, 2022
- iris-bot: dont rely on 'origin' remote being upstream · ad52ed07
  Ralf Jung authored 2 years ago
  
  ad52ed07
Sep 29, 2022
- Bump Iris. · b335afaf
  Robbert Krebbers authored 2 years ago
  
  b335afaf
Sep 25, 2022
- update dependencies · ce054a47
  Ralf Jung authored 2 years ago
  
  ce054a47
Sep 21, 2022
- avoid deprecated fgrep/egrep · 291dc89e
  Ralf Jung authored 2 years ago
  
  fixes #486
  291dc89e
- Merge branch 'pure-exec-mode' into 'master' · ef762697
  Robbert Krebbers authored 2 years ago
  
  add Hint Mode for PureExec See merge request iris/iris!846
  ef762697