Commits · master · Iris / Iris

27 Jan, 2023 1 commit
- Fix indentation. · cc31e712
  Robbert Krebbers authored Jan 21, 2023
  
  cc31e712
08 Jan, 2023 1 commit
- remove some spurious spaces · a34184ae
  Ralf Jung authored Jan 08, 2023
  
  a34184ae
08 Dec, 2022 1 commit
- Merge branch 'robbert/leibnizO' into 'master' · 9e1582b9
  Ralf Jung authored Dec 08, 2022
```
Documentation about `leibnizO`.

See merge request !875
```
  9e1582b9
07 Dec, 2022 1 commit
- No overlapping instances. · b2b13524
  Robbert Krebbers authored Dec 07, 2022
  
  b2b13524
06 Dec, 2022 6 commits
- Address comments Ralf. · 8c7aa6c8
  Robbert Krebbers authored Dec 06, 2022
  
  8c7aa6c8
- Merge branch 'robbert/alt_def' into 'master' · df2362e6
  Ralf Jung authored Dec 06, 2022
```
Rename `sig_{equiv,dist}_alt` into `sig_{equiv,dist}_def` and state using `=` instead of `<->`.

See merge request !877
```
  df2362e6
- Merge branch 'robbert/intuitionistically_alt' into 'master' · 1f0bc79e
  Ralf Jung authored Dec 06, 2022
```
Add lemma `intuitionistically_def P : □ P = <affine> <pers> P`.

See merge request !874
```
  1f0bc79e
- Add lemma `intuitionistically_def P : □ P = <affine> <pers> P`. · 88a5667f
  Robbert Krebbers authored Dec 04, 2022
  
  88a5667f
- CHANGELOG. · 81a42f84
  Robbert Krebbers authored Dec 06, 2022
  
  81a42f84
- Rename `sig_{equiv,dist}_alt` into `sig_{equiv,dist}_def` and state these · e580eac7
  Robbert Krebbers authored Dec 06, 2022
```
lemmas using `=` instead of `<->`.
```
  e580eac7
05 Dec, 2022 4 commits
- Merge branch 'robbert/smaller_iris' into 'master' · b9583c63
  Ralf Jung authored Dec 05, 2022
```
Do not write heading in readme with capitals.

See merge request !876
```
  b9583c63
- move native-compiler flag to be CI-only · 577605fa
  Ralf Jung authored Dec 05, 2022
```
See discussion in https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/iris.20failing
```
  577605fa
- update dependencies · e54dedb4
  Ralf Jung authored Dec 05, 2022
  
  e54dedb4
- Do not write heading in readme with capitals. · 8c90ec66
  Robbert Krebbers authored Dec 05, 2022
  
  8c90ec66
04 Dec, 2022 5 commits
- Paolo's suggestion · 8ebf6025
  Robbert Krebbers authored Dec 04, 2022
  
  8ebf6025
- Say something about boxed types. · c332a0d9
  Robbert Krebbers authored Dec 04, 2022
  
  c332a0d9
- Say more about how to define OFE instances. · 0d5e823b
  Robbert Krebbers authored Dec 04, 2022
  
  0d5e823b
- Documentation about `leibnizO`. · 23b1b0c3
  Robbert Krebbers authored Dec 04, 2022
  
  23b1b0c3
- Type annotation in potential ambigious case. · 002cb824
  Robbert Krebbers authored Dec 04, 2022
  
  002cb824
30 Nov, 2022 3 commits
- bump CI to Coq 8.16.1 · e52255ba
  Ralf Jung authored Nov 30, 2022
  
  e52255ba
- update dependencies · 974fa2f7
  Ralf Jung authored Nov 30, 2022
  
  974fa2f7
- update dependencies · db6cb399
  Ralf Jung authored Nov 30, 2022
  
  db6cb399
29 Nov, 2022 4 commits
- update dependencies · de908f52
  Ralf Jung authored Nov 29, 2022
  
  de908f52
- make lc_supply Local · c44ce4c9
  Ralf Jung authored Nov 29, 2022
  
  c44ce4c9
- Merge branch 'fupd-soundness' into 'master' · d48b71ab
  Ralf Jung authored Nov 29, 2022
```
slightly generalize and reorganize fupd soundness lemmas

See merge request !863
```
  d48b71ab
- simplify proof script a bit · 3934a80f
  Robbert Krebbers authored Nov 29, 2022 and Ralf Jung committed Nov 29, 2022
  
  3934a80f
27 Nov, 2022 1 commit
- Merge branch 'fractional-embed' into 'master' · c05dacc5
  Robbert Krebbers authored Nov 27, 2022
```
Add Fractional and AsFractional instance for embed

See merge request !868
```
  c05dacc5
26 Nov, 2022 1 commit
- Add Fractional and AsFractional instance for embed · 4df29af7
  Simon Friis Vindum authored Nov 21, 2022
  
  4df29af7
24 Nov, 2022 10 commits
- Merge branch 'robbert/gset_solver' into 'master' · 5b5d3f4d
  Ralf Jung authored Nov 24, 2022
```
Add (basic) support for `gset` and `gset_disj` cameras to `set_solver`.

See merge request !871
```
  5b5d3f4d
- CHANGELOG. · e35c8ee0
  Robbert Krebbers authored Nov 24, 2022
  
  e35c8ee0
- Tests. · eaca0845
  Robbert Krebbers authored Nov 24, 2022
  
  eaca0845
- Add basic support for `gset_disj` to `set_solver`. · 3b184486
  Robbert Krebbers authored Nov 24, 2022
  
  3b184486
- Add support for `gset` camera to `set_solver`. · 51278834
  Robbert Krebbers authored Nov 24, 2022
  
  51278834
- Merge branch 'robbert/solve_tc' into 'master' · 4d4f4192
  Robbert Krebbers authored Nov 24, 2022
```
Remove tactic `iSolveTC` in favor of `tc_solve` in std++.

See merge request !870
```
  4d4f4192
- CHANGELOG. · f7271e52
  Robbert Krebbers authored Nov 24, 2022
  
  f7271e52
- Remove tactic `iSolveTC`. · 893f1ab0
  Robbert Krebbers authored Nov 24, 2022
  
  893f1ab0
- Bump std++. · 70f443db
  Robbert Krebbers authored Nov 24, 2022
  
  70f443db
- make one_shot_once example a bit more idiomatic · 7481461f
  Ralf Jung authored Nov 24, 2022
  
  7481461f
23 Nov, 2022 2 commits
- add GSet_inj · ebd33ba0
  Ralf Jung authored Nov 23, 2022
  
  ebd33ba0
- Merge branch 'heaplang.sty-hyperref' into 'master' · 2850b92a
  Ralf Jung authored Nov 23, 2022
```
heaplang.sty: avoid clash with hyperref

Closes #489

See merge request !858
```
  2850b92a