Commits · 06e1a5e7f912713db83b825d83ddc715e64e88e8 · Jules Jacobs / Iris

19 Mar, 2020 1 commit
- Add VS code to the editor.md docs · 06e1a5e7
  Jules Jacobs authored Mar 19, 2020
  
  06e1a5e7
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 iris/iris!393
```
  a9043adb
- vdash changelog · ba7879fc
  Ralf Jung authored Mar 16, 2020
  
  ba7879fc
- Merge branch 'explicit-vdash' into 'master' · 62be0a86
  Robbert authored Mar 16, 2020
```
Explicit vdash

See merge request iris/iris!358
```
  62be0a86
- CLEAN cleanup · 31bb46c5
  Gregory Malecha authored 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 iris/iris!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 authored Mar 12, 2020
```
Close issue #299: `leibnizO` finds convoluted proof for definitions

Closes #299

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

See merge request iris/iris!391
```
  79f576aa
- Testcase for iris/stdpp!123 . · 0edc1504
  Robbert Krebbers authored Mar 10, 2020
  
  0edc1504
- Merge branch 'robbert/fill' into 'master' · 3ffb9bc9
  Robbert authored Mar 10, 2020
```
More consistent names for `fill` lemmas of `LanguageCtx`.

See merge request iris/iris!389
```
  3ffb9bc9
- CHANGELOG. · 8cd78942
  Robbert Krebbers authored Mar 10, 2020
  
  8cd78942
- More consistent names for `fill` lemmas of `LanguageCtx`. · 29c4fcf6
  Robbert Krebbers authored Mar 09, 2020
```
Use `_inv` for the reverse direction.
```
  29c4fcf6
- Add lemma `fupd_plain_laterN`. · eb200cc0
  Robbert Krebbers authored Mar 10, 2020
  
  eb200cc0
- Add lemma `except_0_laterN`. · ea869f3b
  Robbert Krebbers authored Mar 10, 2020
  
  ea869f3b
- Merge branch 'ralf/later-equiv' into 'master' · 6950ddde
  Ralf Jung authored Mar 10, 2020
```
prove later commuting around equality one way

See merge request iris/iris!388
```
  6950ddde
- rename later_equivI_prop for consistency · 49530cb3
  Ralf Jung authored Mar 10, 2020
  
  49530cb3
- refactor proof (by Robbert) · 56a8f794
  Ralf Jung authored Mar 10, 2020
  
  56a8f794
- bump std++ · c40de17c
  Ralf Jung authored Mar 10, 2020
  
  c40de17c
- copy text from BSD-3 template · df9f373a
  Ralf Jung authored Mar 04, 2020
  
  df9f373a
- Add lemma `except_0_into_later P : ◇ P ⊢ ▷ P`. · 81685f69
  Robbert Krebbers authored Mar 09, 2020
  
  81685f69
- Merge branch 'avoid-constr-hints' into 'master' · c71c9250
  Robbert authored Mar 10, 2020
```
Avoid using Hint Resolve with a term

See merge request iris/iris!390
```
  c71c9250
- Avoid using Hint Resolve with a term · ba7e4c46
  Tej Chajed authored Mar 10, 2020
```
This feature is now deprecated in Coq master (see
https://github.com/coq/coq/pull/7791).

Instead of passing a partially-applied lemma directly to Hint Resolve,
first create a definition and then make that reference a hint.
```
  ba7e4c46
09 Mar, 2020 1 commit
- Make better use of `not_stuck` in adequacy. · 179725af
  Robbert Krebbers authored Mar 09, 2020
  
  179725af
06 Mar, 2020 1 commit
- prove later commuting around equality one way · a9b6aa75
  Ralf Jung authored Mar 06, 2020
  
  a9b6aa75