Commits · ed4332632775eb6d5ce50f4baa6de534c385e726 · Iris / Iris

17 Jan, 2022 14 commits
- changelog · ed433263
  Ralf Jung authored Jan 17, 2022
  
  ed433263
- remove _frac_ lemmas, the corresponding _dfrac_ lemmas are sufficient · ad579807
  Ralf Jung authored Jan 14, 2022
  
  ad579807
- make mono_list_auth DfracDiscarded notation consistent · d7e80d10
  Ralf Jung authored Dec 16, 2021
  
  d7e80d10
- unstage mono_list algebra · a9ebd972
  Ralf Jung authored Nov 29, 2021
  
  a9ebd972
- Merge branch 'ralf/mono_nat' into 'master' · ec624937
  Ralf Jung authored Jan 17, 2022
```
mono_nat algebra: add dfrac support and notation

See merge request !759
```
  ec624937
- Merge branch 'ci/ralf/frame-frac' into 'master' · 901016fc
  Ralf Jung authored Jan 17, 2022
```
don't make frame_fractional an instance

Closes #351

See merge request !739
```
  901016fc
- changelog · 230ff113
  Ralf Jung authored Dec 16, 2021
  
  230ff113
- remove _frac_ lemmas, the corresponding _dfrac_ lemmas are sufficient · 41e81796
  Ralf Jung authored Jan 14, 2022
  
  41e81796
- swap direction of mono_nat_lb_op · 1503fb75
  Ralf Jung authored Dec 16, 2021
  
  1503fb75
- mono_nat algebra: add dfrac support and notation · c7cda88a
  Ralf Jung authored Nov 29, 2021
  
  c7cda88a
- Merge branch 'ralf/auth_frac_op' into 'master' · 347533aa
  Ralf Jung authored Jan 17, 2022
```
remove auth_frac_op lemmas

See merge request !774
```
  347533aa
- changelog · d38ec11e
  Ralf Jung authored Jan 16, 2022
  
  d38ec11e
- add back explicit framing instance for ↦ · fd49bcbe
  Ralf Jung authored Nov 29, 2021
  
  fd49bcbe
- perf experiment: dont make frame_fractional an instance · ea51b43b
  Ralf Jung authored Sep 30, 2021
  
  ea51b43b
15 Jan, 2022 3 commits
- Merge branch 'ralf/dfrac_agree' into 'master' · 52c80aad
  Ralf Jung authored Jan 15, 2022
```
rename the new dfrac_agree update lemmas for consistency

See merge request !769
```
  52c80aad
- rename the new dfrac_agree update lemmas for consistency · 2e07f003
  Ralf Jung authored Dec 17, 2021
  
  2e07f003
- remove auth_frac_op lemmas · 64825c1c
  Ralf Jung authored Jan 14, 2022
  
  64825c1c
14 Jan, 2022 2 commits
- Merge branch 'pr-13969-take3' into 'master' · f85824ee
  Robbert Krebbers authored Jan 14, 2022
```
Fix bi_rewrite_relation hint priority

See merge request !773
```
  f85824ee
- Fix bi_rewrite_relation hint priority · a9140f8e
  Matthieu Sozeau authored Jan 14, 2022 and Robbert Krebbers committed Jan 14, 2022
  
  a9140f8e
13 Jan, 2022 1 commit
- Bump std++. · 5070f7f5
  Robbert Krebbers authored Jan 13, 2022
  
  5070f7f5
12 Jan, 2022 1 commit
- Bump stdpp. · 8b085901
  Robbert Krebbers authored Jan 12, 2022
  
  8b085901
11 Jan, 2022 4 commits
- Merge branch 'is_closed_gset' into 'master' · b0d820ff
  Robbert Krebbers authored Jan 11, 2022
```
Formulate `is_closed_expr` in terms of `gset`s.

See merge request !707
```
  b0d820ff
- Update documentation & changelog · 9fae57da
  Dan Frumin authored Dec 30, 2021
  
  9fae57da
- Tweak proofs. · bc626812
  Robbert Krebbers authored Dec 11, 2021
  
  bc626812
- Formulate `is_closed_expr` in terms of `gset`s. · ea4d05c6
  Dan Frumin authored Jun 20, 2021
```
And prove some additional lemmas.
```
  ea4d05c6
30 Dec, 2021 2 commits
- Merge branch 'master' into 'master' · f6beee55
  Ralf Jung authored Dec 30, 2021
```
Fix name, `Later_inj` -> `Next_inj`.

See merge request !770
```
  f6beee55
- `Later_inj` -> `Next_inj`. · 46595d5c
  Dan Frumin authored Dec 30, 2021 and Ralf Jung committed Dec 30, 2021
  
  46595d5c
17 Dec, 2021 6 commits
- Merge branch 'telescope-notation' into 'master' · ec0acc9c
  Ralf Jung authored Dec 17, 2021
```
simplify telescope-based notations

See merge request !762
```
  ec0acc9c
- simplify telescope-based notations · ea0b55fa
  Ralf Jung authored Nov 30, 2021
```
These type annotations are no longer needed once we have a bidirectionality hint
on tele_app.
```
  ea0b55fa
- Merge branch 'ralf/drop-8.12' into 'master' · 6dfda15b
  Ralf Jung authored Dec 17, 2021
```
drop support for Coq 8.12

See merge request !763
```
  6dfda15b
- drop support for Coq 8.12 · f3b02428
  Ralf Jung authored Dec 03, 2021
  
  f3b02428
- Merge branch 'ralf/dfrac_agree' into 'master' · 72485828
  Ralf Jung authored Dec 17, 2021
```
equip frac_agree with support for dfrac

See merge request !766
```
  72485828
- coqdocify · 047d1fa5
  Robbert Krebbers authored Dec 17, 2021 and Ralf Jung committed Dec 17, 2021
  
  047d1fa5
16 Dec, 2021 7 commits
- Merge branch 'add-proofmode-tests' into 'master' · c259c060
  Ralf Jung authored Dec 16, 2021
```
Add tests for iRename, iTypeOf, and iInduction with multiple IHs

Closes #334

See merge request !768
```
  c259c060
- Add tests for iRename, iTypeOf, and iInduction with multiple IHs · 7f3a9fa8
  Tej Chajed authored Dec 16, 2021 and Ralf Jung committed Dec 16, 2021
  
  7f3a9fa8
- to_frac_agree is deliberately transparent · 93f9452c
  Ralf Jung authored Dec 16, 2021
  
  93f9452c
- add Params · 5c98c9a8
  Ralf Jung authored Dec 16, 2021
  
  5c98c9a8
- equip frac_agree with support for dfrac · f3cc33ae
  Ralf Jung authored Dec 12, 2021
  
  f3cc33ae
- frac_agree: make validity lemmas bidirectional, add update_2 lemma and use it for ghost_var · a68723bb
  Ralf Jung authored Dec 12, 2021
  
  a68723bb
- bump std++. · 7c7054b9
  Robbert Krebbers authored Dec 16, 2021
  
  7c7054b9