Commits · a3534b51226f93379b1ec75367f33ae68b81a5d0 · Pierre Roux / Iris

May 13, 2022
- CHANGELOG. · a3534b51
  Robbert Krebbers authored 2 years ago
  
  a3534b51
- No longer make `envs_entails_unseal` local. · 599493de
  Robbert Krebbers authored 2 years ago
  
  599493de
- Make unseal collections `Local`. · 419e96d8
  Robbert Krebbers authored 2 years ago
  
  419e96d8
- Rename seal lemmas from `_eq` to `_unseal` and make sealing stuff `Local`. · 088999ea
  Robbert Krebbers authored 2 years ago
  
  Also fix some places where we break the seal.
  088999ea
- Bump std++. · a44ffc04
  Robbert Krebbers authored 2 years ago
  
  a44ffc04
- fix some coqdoc warnings · e706afbf
  Ralf Jung authored 2 years ago
  
  e706afbf
- Merge branch 'ralf/dom' into 'master' · a1971471
  Ralf Jung authored 2 years ago
  
  port to dom D type being implicit See merge request iris/iris!795
  a1971471
- bump std++; port to dom D type being implicit · 9f0eb79d
  Ralf Jung authored 2 years ago
  
  9f0eb79d
May 11, 2022
- Merge branch 'indentations' into 'master' · dacf718e
  Ralf Jung authored 2 years ago
  
  Updated suggested emacs indendation configuration See merge request iris/iris!776
  dacf718e
- Updated suggested emacs indendation configuration · 6df13ca8
  Jonas Kastberg authored 2 years ago and Ralf Jung committed 2 years ago
  
  6df13ca8
May 09, 2022
- Merge branch 'ralf/big_sepS' into 'master' · 0b89b550
  Ralf Jung authored 2 years ago
  
  add big_sepS_insert_2' and big_sepS_union_2 See merge request iris/iris!787
  0b89b550
- strengthen big_sepS_union_2 · 608e43fe
  Robbert Krebbers authored 2 years ago and Ralf Jung committed 2 years ago
  
  608e43fe
- add big_sepS_insert_2' and big_sepS_union_2 · 75700c31
  Ralf Jung authored 2 years ago
  
  75700c31
May 08, 2022
- normalize OCaml versions · 2f1129aa
  Ralf Jung authored 2 years ago
  
  2f1129aa
May 07, 2022
- fix accidental use of coPset domain · 8ce92349
  Ralf Jung authored 2 years ago
  
  8ce92349
May 06, 2022
- stop using coPset · bc1afae4
  Ralf Jung authored 2 years ago
  
  bc1afae4
- Merge branch 'fixpoint-tele_arg' into 'master' · 1414d845
  Ralf Jung authored 2 years ago
  
  Pick universes for [bi_tforall] and [bi_texist]. See merge request iris/iris!781
  1414d845
- Pick and name universes for [bi_tforall] and [bi_texist]. · 171768c4
  Gregory Malecha authored 3 years ago and Ralf Jung committed 2 years ago
  
  This requires the [fixpoint] version of [tele_arg].
  171768c4
- looks like there is no 4.13.2 · 7b9f809f
  Ralf Jung authored 2 years ago
  
  7b9f809f
- bump ocaml version · e8a52a12
  Ralf Jung authored 2 years ago
  
  e8a52a12
May 04, 2022
- Merge branch 'stdpp-bump' into 'master' · 10e843d9
  Ralf Jung authored 2 years ago
  
  Bump stdpp to include telescope fixes See merge request iris/iris!790
  10e843d9
- Bump stdpp to include telescope fixes · bfb0142f
  Paolo G. Giarrusso authored 2 years ago
  
  bfb0142f
May 01, 2022
- Merge branch 'robbert/iRevert_pure' into 'master' · 5fa30a35
  Robbert Krebbers authored 2 years ago
  
  Let `iRevert` of a pure hypotheses generate a wand instead of implication. See merge request !789
  5fa30a35
- Merge branch 'robbert/iApply_pretty' into 'master' · e785e4a0
  Robbert Krebbers authored 2 years ago
  
  Fix bug in `iApply` prettification. See merge request iris/iris!788
  e785e4a0
- Apply 1 suggestion(s) to 1 file(s) · 83256c1d
  Ralf Jung authored 2 years ago and Robbert Krebbers committed 2 years ago
  
  83256c1d
- Apply 1 suggestion(s) to 1 file(s) · 854dcaaf
  Ralf Jung authored 2 years ago and Robbert Krebbers committed 2 years ago
  
  854dcaaf
- fix changelog style · 9d04874f
  Ralf Jung authored 2 years ago
  
  9d04874f
Apr 23, 2022
- CHANGELOG. · 5f73bf42
  Robbert Krebbers authored 2 years ago
  
  5f73bf42
- Tests. · e440e51b
  Robbert Krebbers authored 2 years ago
  
  e440e51b
- `iRevert` of a pure hypotheses generates a wand instead of implication. · 2bea47fc
  Robbert Krebbers authored 2 years ago
  
  2bea47fc
Apr 20, 2022
- Fix bug in `iApply` prettification. · 3121e4ed
  Robbert Krebbers authored 2 years ago
  
  3121e4ed
Apr 12, 2022
- update dependencies · a3bed7ea
  Ralf Jung authored 2 years ago
  
  a3bed7ea
Apr 11, 2022
- update dependencies · a4f8cf17
  Ralf Jung authored 2 years ago
  
  a4f8cf17
Apr 10, 2022
- Merge branch 'later_stripping' into 'master' · b6bc287b
  Robbert Krebbers authored 2 years ago
  
  Added capability for stripping multiple laters per step in HeapLang See merge request iris/iris!783
  b6bc287b
- Added capability for stripping multiple laters per step in HeapLang · dd53c9a9
  Jonas Kastberg authored 2 years ago and Robbert Krebbers committed 2 years ago
  
  dd53c9a9
Apr 08, 2022

Merge branch 'robbert/siProp_scope' into 'master' · 316257fb

Dump `siProp_scope` and use `bi_scope`. This is consistent with `uPred`.

See merge request iris/iris!786

316257fb

Apr 07, 2022
- Trailing newline. · b034fd49
  Robbert Krebbers authored 2 years ago
  
  b034fd49
- Comments. · 82b8ee7d
  Robbert Krebbers authored 2 years ago
  
  82b8ee7d
- Merge branch 'robbert/bi_cofe' into 'master' · 456db30e
  Robbert Krebbers authored 2 years ago
  
  Ensure that different `Cofe` proofs of `iProp` are convertible. See merge request iris/iris!784
  456db30e
- Ensure that different `Cofe` proofs of `iProp` are convertible. · 00d2fb63
  Robbert Krebbers authored 2 years ago
  
  00d2fb63