Commits · 51a8187936931afd37fe5a812bfbb8ebd749421b · Pierre Roux / Iris

Nov 10, 2021
- this is now the Iris 3.6 docs · 51a81879
  Ralf Jung authored 3 years ago
  
  51a81879
Nov 09, 2021
- Merge branch 'ralf/fixpoint_unfold' into 'master' · d87541bc
  Ralf Jung authored 3 years ago
  
  give some help for using fixpoint_unfold See merge request iris/iris!749
  d87541bc
Nov 08, 2021
- Merge branch 'ralf/persistently-forall' into 'master' · 53ec94ec
  Ralf Jung authored 3 years ago
  
  move persistently_forall_2 out of BI interface See merge request !702
  53ec94ec
- tweak changelog · 049ac8e3
  Robbert Krebbers authored 3 years ago and Ralf Jung committed 3 years ago
  
  049ac8e3
- changelog · 72d9cb6e
  Ralf Jung authored 3 years ago
  
  72d9cb6e
- give some help for using fixpoint_unfold · d4dd8716
  Ralf Jung authored 3 years ago
  
  d4dd8716
- Merge branch 'ralf/big_sepL2_sep' into 'master' · dd9a044e
  Ralf Jung authored 3 years ago
  
  lemmas to merge a sepL and a sepL2 See merge request !735
  dd9a044e
- GPFSL supports timing now · bdad8ab2
  Ralf Jung authored 3 years ago
  
  bdad8ab2
- formatting and nits · b0eb3ed9
  Ralf Jung authored 3 years ago
  
  b0eb3ed9
- improve comments · 6db3649f
  Robbert Krebbers authored 3 years ago and Ralf Jung committed 3 years ago
  
  6db3649f
- fix spacing · ce6f4e19
  Paolo G. Giarrusso authored 3 years ago and Ralf Jung committed 3 years ago
  
  ce6f4e19
- move persistently_forall_2 out of BI interface · 89b76adb
  Ralf Jung authored 3 years ago
  
  89b76adb
- Merge branch 'fixpoint-lemmas' into 'master' · c1c08c1b
  Ralf Jung authored 3 years ago
  
  bi/fixpoint lemmas See merge request !725
  c1c08c1b
- dedup contributor list · 8a143c4e
  Ralf Jung authored 3 years ago
  
  8a143c4e
Nov 06, 2021
- more attribution in changelog · e7c8a262
  Ralf Jung authored 3 years ago
  
  e7c8a262
- Fixpoint/Cofixpoint lemmas · 3cf98386
  Lennard Gäher authored 3 years ago
  
  3cf98386
Nov 05, 2021
- finalize release · efb686ba
  Ralf Jung authored 3 years ago
  
  iris-3.5.0
  
  efb686ba
- Merge branch 'release-notes-3.5.0' into 'master' · 96a25e2d
  Ralf Jung authored 3 years ago
  
  Iris 3.5.0 release notes Closes #435 See merge request iris/iris!748
  96a25e2d
- Iris 3.5.0 release notes · 058a7bb2
  Tej Chajed authored 3 years ago and Ralf Jung committed 3 years ago
  
  058a7bb2
- empty commit to re-trigger CI · b7cd5b97
  Ralf Jung authored 3 years ago
  
  b7cd5b97
- test 8.14.0 and coq master · c4156809
  Ralf Jung authored 3 years ago
  
  c4156809
Oct 27, 2021
- Merge branch 'robbert/asfractional' into 'master' · 90b6007f
  Robbert Krebbers authored 3 years ago
  
  Improve documentation of convention for `AsFractional` instances See merge request !747
  90b6007f
Oct 26, 2021
- Merge branch 'ralf/opam-desc' into 'master' · d4fc6c46
  Ralf Jung authored 3 years ago
  
  update package descriptions Closes #436 See merge request !746
  d4fc6c46
- Comment about `AsFractional` instances. · 3f5c467b
  Robbert Krebbers authored 3 years ago
  
  3f5c467b
- Merge branch 'fractional_big_sepL2' into 'master' · fb763c47
  Ralf Jung authored 3 years ago
  
  Prove missing fractional_big_sepL2 See merge request !737
  fb763c47
- update package descriptions · be23bc6a
  Ralf Jung authored 3 years ago
  
  be23bc6a
- fractional_big_sep*: uniform type annotations · 3162a652
  Paolo G. Giarrusso authored 3 years ago
  
  To match the suggestion in !737 (comment 75017).
  Verified
  
  3162a652
- Prove missing fractional_big_sepL2 · 830e8148
  Paolo G. Giarrusso authored 3 years ago
  
  Verified
  
  830e8148
Oct 25, 2021
- Move more proofs out of section. · 060db655
  Robbert Krebbers authored 3 years ago
  
  060db655
- Move proof out of section and shorten it. · c6a67c43
  Robbert Krebbers authored 3 years ago
  
  c6a67c43
Oct 19, 2021
- Fix coqdoc rendering · 12925885
  Ralf Jung authored 3 years ago
  
  fixes #437
  12925885
Oct 15, 2021
- Merge branch 'editor-doc-vim' into 'master' · bacc5968
  Ralf Jung authored 3 years ago
  
  Editor docs: add information on how to use vim for working with Iris See merge request iris/iris!744
  bacc5968
- vim editor docs · 778e70ed
  Lennard Gäher authored 3 years ago
  
  778e70ed
Oct 13, 2021

Merge branch 'adjust-focused-goal' into 'master' · 3b9231eb
Ralf Jung authored 3 years ago
```
Normalize focused goal output

See merge request iris/iris!743
```
3b9231eb

Normalize focused goal output · fd8f6c52

Tej Chajed authored 3 years ago

Merge the "1 focused goal" line with the subsequent "(shelved: 1)" line,
since this is the new output in Coq 8.15+.

Iris does not currently produce this output, since no test calls `Show`
with shelved goals, but this future-proofs the test normalization.

Verified

fd8f6c52

Oct 11, 2021
- Fix indentation. · cd511950
  Robbert Krebbers authored 3 years ago
  
  cd511950
Oct 02, 2021
- Merge branch 'ralf/f_contractive' into 'master' · db5bd60a
  Ralf Jung authored 3 years ago
  
  make f_contractive consistent with f_equiv See merge request !741
  db5bd60a
- make f_contractive consistent with f_equiv · 1d937ab3
  Ralf Jung authored 3 years ago
  
  1d937ab3
- Merge branch 'ralf/as-frac-mode' into 'master' · 9ed67339
  Ralf Jung authored 3 years ago
  
  relax AsFractional Hint Mode See merge request iris/iris!740
  9ed67339
- Merge branch 'optimize_iDestruct' into 'master' · f8ca8f5b
  Robbert Krebbers authored 3 years ago
  
  Optimize iDestruct by avoiding superfluous iRenames See merge request !733
  f8ca8f5b