Commits · e5a2bcfff486137a25b28e4d574638ac52fd1d84 · Lennard Gäher / Iris

27 Mar, 2020 1 commit
- sbi_internal_eq: add "sections" of notation, following stdpp · e5a2bcff
  Paolo G. Giarrusso authored Mar 27, 2020
  
  e5a2bcff
25 Mar, 2020 4 commits
- Merge branch 'robbert/atomic_wp_seq_step' into 'master' · ab3b5c77
  Ralf Jung authored Mar 25, 2020
```
Prove stepping (i.e., non-value) version of `atomic_wp_seq`.

See merge request !402
```
  ab3b5c77
- Prove stepping (i.e., non-value) version of `atomic_wp_seq`. · eae9c2c8
  Robbert Krebbers authored Mar 25, 2020
  
  eae9c2c8
- Merge branch 'robbert/exist_laterable' into 'master' · 3c2ea188
  Ralf Jung authored Mar 25, 2020
```
Prove `Laterable (∃ x, Φ x)`.

See merge request iris/iris!401
```
  3c2ea188
- Prove `Laterable (∃ x, Φ x)`. · d3a4d722
  Robbert Krebbers authored Mar 25, 2020
  
  d3a4d722
23 Mar, 2020 1 commit
- Remove redundant space. · 3a0d7152
  Robbert Krebbers authored Mar 23, 2020
  
  3a0d7152
21 Mar, 2020 2 commits
- Merge branch 'vscode-editor-docs' into 'master' · ed3b52f9
  Robbert Krebbers authored Mar 21, 2020
```
Add VS code to the editor.md docs

See merge request iris/iris!397
```
  ed3b52f9
- Add VS code to the editor.md docs · b32af454
  Jules Jacobs authored Mar 21, 2020 and Robbert Krebbers committed Mar 21, 2020
  
  b32af454
20 Mar, 2020 8 commits
- Merge branch 'robbert/iAssumption' into 'master' · 3f069634
  Robbert Krebbers authored Mar 20, 2020
```
Make `iAssumption` work on `⊢ ...` premises in the Coq context.

See merge request iris/iris!398
```
  3f069634
- Add documentation. · ba3f6ce2
  Robbert Krebbers authored Mar 20, 2020
  
  ba3f6ce2
- CHANGELOG entry. · f7e06e4d
  Robbert Krebbers authored Mar 20, 2020
  
  f7e06e4d
- Make `iAssumption` work on `⊢ ...` premises in the Coq context. · ef68c7c4
  Robbert Krebbers authored Jan 21, 2020
  
  ef68c7c4
- Fix errors of `iAssumption`, `iExact`, and friends. · 1e00275c
  Robbert Krebbers authored Mar 19, 2020
```
- The error messages were wrong: the goal needs to be absorbing, not the hypothesis.
- The wrong failure number was used in `iAssumption`, which caused the error not
  to be propagated properly.
```
  1e00275c
- Fix bad line break. · a7b4c684
  Robbert Krebbers authored Mar 20, 2020
  
  a7b4c684
- Instance for `Affine (□?p P)`. · 2e4bd8f5
  Robbert Krebbers authored Mar 20, 2020
  
  2e4bd8f5
- update dependencies · 564719a4
  Ralf Jung authored Mar 20, 2020
  
  564719a4
19 Mar, 2020 1 commit
- Fix Coqdoc. · 4875791a
  Robbert Krebbers authored Mar 19, 2020
  
  4875791a
18 Mar, 2020 11 commits
- Merge branch 'ci/ralf/pair_core_id' into 'master' · d157edcc
  Ralf Jung authored Mar 18, 2020
```
Use apply: for pair_core_id

Closes #255

See merge request iris/iris!395
```
  d157edcc
- Avoid slow `try done`. · 287cfd91
  Robbert Krebbers authored Mar 18, 2020
  
  287cfd91
- change some other hints to a more general pattern and typeclass instances · 9c47194e
  Ralf Jung authored Mar 18, 2020
  
  9c47194e
- add regression test · 042cbada
  Ralf Jung authored Mar 18, 2020
  
  042cbada
- make pair_core_id a new-unification-instance · 6afa0332
  Ralf Jung authored Mar 18, 2020
  
  6afa0332
- definitionally -> propositionally · 26d4f967
  Ralf Jung authored Mar 18, 2020
  
  26d4f967
- Merge branch 'ralf/masks' into 'master' · 39850eac
  Ralf Jung authored Mar 18, 2020
```
mention that masks in Coq are a bit different than on paper

Closes #211

See merge request iris/iris!394
```
  39850eac
- mention that masks in Coq are a bit different than on paper · 6ba36cd6
  Ralf Jung authored Mar 18, 2020
  
  6ba36cd6
- Turn some forgotten uses of `bi_emp_valid` into the new `⊢` notation. · 3442e7ae
  Robbert Krebbers authored Mar 18, 2020
  
  3442e7ae
- build-all: fix lambda-rust weak_mem branch · ad3a71bf
  Ralf Jung authored Mar 18, 2020
  
  ad3a71bf
- update dependencies; fix for fmap_seq rename · b815eba9
  Ralf Jung authored Mar 18, 2020
  
  b815eba9
16 Mar, 2020 4 commits
- Merge branch 'ralf/vdash-changelog' into 'master' · a9043adb
  Ralf Jung authored Mar 16, 2020
```
vdash changelog

See merge request !393
```
  a9043adb
- vdash changelog · ba7879fc
  Ralf Jung authored Mar 16, 2020
  
  ba7879fc
- Merge branch 'explicit-vdash' into 'master' · 62be0a86
  Robbert Krebbers authored Mar 16, 2020
```
Explicit vdash

See merge request !358
```
  62be0a86
- CLEAN cleanup · 31bb46c5
  Gregory Malecha authored Mar 16, 2020 and Robbert Krebbers committed Mar 16, 2020
```
- remove "odd" comment
- move atomic triples to bi_scope
```
  31bb46c5
13 Mar, 2020 4 commits
- license: remove unnecessary header with typo · ad82d138
  Ralf Jung authored Mar 13, 2020
  
  ad82d138
- Merge branch 'jung-master-patch-98309' into 'master' · 7fcb2969
  Ralf Jung authored Mar 13, 2020
```
fill in blanks in license

See merge request !387
```
  7fcb2969
- the old docs/ folder moved to tex/ · 0d32b394
  Ralf Jung authored Mar 13, 2020
  
  0d32b394
- add copyright notice · 017862b0
  Ralf Jung authored Mar 13, 2020
  
  017862b0
12 Mar, 2020 3 commits
- Fix typo. · 9f19f1ab
  Robbert Krebbers authored Mar 12, 2020
  
  9f19f1ab
- Merge branch 'robbert/issue299' into 'master' · 232a2e93
  Robbert Krebbers authored Mar 12, 2020
```
Close issue #299: `leibnizO` finds convoluted proof for definitions

Closes #299

See merge request !392
```
  232a2e93
- Close issue #299: `leibnizO` finds convoluted proof for definitions · f2eabe78
  Robbert Krebbers authored Mar 12, 2020
  
  f2eabe78
10 Mar, 2020 1 commit
- Merge branch 'robbert/TCEq_hint' into 'master' · 79f576aa
  Robbert Krebbers authored Mar 10, 2020
```
Testcase for iris/stdpp!123.

See merge request iris/iris!391
```
  79f576aa