Commits · 55283d57c9c2a6c997f5e77d66c3d575da7965ed · Jonas Kastberg / iris

25 Feb, 2020 1 commit
- bump std++, and fix for rename · 55283d57
  Ralf Jung authored Feb 25, 2020
  
  55283d57
23 Feb, 2020 4 commits
- Merge branch 'fix-twp_allocN-tac' into 'master' · 802035a5
  Robbert Krebbers authored Feb 23, 2020
```
Fix wp_alloc when applying twp_allocN

See merge request iris/iris!382
```
  802035a5
- Fix wp_alloc when applying twp_allocN · c2d9ad1d
  Tej Chajed authored Feb 23, 2020 and Robbert Krebbers committed Feb 23, 2020
  
  c2d9ad1d
- Merge branch 'array-fraction' into 'master' · 40c0674a
  Robbert Krebbers authored Feb 23, 2020
```
Add ownership fraction to array assertion

See merge request iris/iris!380
```
  40c0674a
- Add ownership fraction to array assertion · 54fb1312
  Tej Chajed authored Feb 23, 2020
  
  54fb1312
20 Feb, 2020 2 commits
- Merge branch 'ralf/modalities' into 'master' · 4815e68e
  Ralf Jung authored Feb 20, 2020
```
say things about modalities

See merge request iris/iris!377
```
  4815e68e
- say things about modalities · 8bc5a88a
  Ralf Jung authored Feb 20, 2020
  
  8bc5a88a
19 Feb, 2020 5 commits
- re-enable coqchk on coq master, for testing · 7ddea37a
  Ralf Jung authored Feb 19, 2020
  
  7ddea37a
- Bump std++. · 96f40f26
  Robbert Krebbers authored Feb 19, 2020
  
  96f40f26
- also build nightly against known-to-work Coq version · be509a69
  Ralf Jung authored Feb 19, 2020
  
  be509a69
- CI: test Coq 8.11.dev on pushes, and master nightly · 8f75516d
  Ralf Jung authored Feb 19, 2020
  
  8f75516d
- temporarily disable broken coqchk · beb9d445
  Ralf Jung authored Feb 19, 2020
  
  beb9d445
18 Feb, 2020 15 commits
- Merge branch 'robbert/intuitionistic_inv' into 'master' · 45383da9
  Ralf Jung authored Feb 18, 2020
```
Add introduction pattern `-# pat` to move a hypothesis to the spatial context

Closes #213

See merge request iris/iris!370
```
  45383da9
- Remove more new lines. · 00bd9cf1
  Robbert Krebbers authored Feb 18, 2020
  
  00bd9cf1
- And more useless new lines. · 461c88d6
  Robbert Krebbers authored Feb 18, 2020
  
  461c88d6
- Remove useless newlines in `proof_mode.md`. · 1a5d7d58
  Robbert Krebbers authored Feb 18, 2020
  
  1a5d7d58
- CHANGELOG entry for the `-# pat` intro pattern. · e9e00698
  Robbert Krebbers authored Feb 05, 2020
  
  e9e00698
- Add tests for the `-# pat` intro pattern. · e53c2699
  Robbert Krebbers authored Feb 05, 2020
  
  e53c2699
- Add proof mode documentation for the `-# pat` intro pattern. · 226b8579
  Robbert Krebbers authored Feb 05, 2020
  
  226b8579
- Improve docs of the `# pat` intro pattern. · 25061957
  Robbert Krebbers authored Feb 18, 2020
  
  25061957
- Add `-# pat` intro pattern to move a hypothesis to the spatial context. · c6a5d2d6
  Robbert Krebbers authored Feb 05, 2020
  
  c6a5d2d6
- Stop using deprecated `!#` intro pattern. · 91cfdc1e
  Robbert Krebbers authored Feb 18, 2020
  
  91cfdc1e
- Stop using deprecated `iAlways` tactic. · acd32497
  Robbert Krebbers authored Feb 18, 2020
  
  acd32497
- Mark `iAlways` as deprecated in the code. · ad7eeccc
  Robbert Krebbers authored Feb 18, 2020
```
It was already marked as deprecated in `doc/proof_mode.md`.
```
  ad7eeccc
- Make names of constructors of `intro_pat` consistent with names of `tac_` lemmas. · 066b7f65
  Robbert Krebbers authored Feb 18, 2020
```
- Rename `IPureElim` -> `iPure`, `IAlwaysElim` -> `IIntuitionistic`
- Drop `IAlwaysIntro` (it's just `IModalIntro`).
```
  066b7f65
- add another printing hint for normalization · 3b0457d4
  Ralf Jung authored Feb 18, 2020
  
  3b0457d4
- note that 'Set Ltac Backtrace' is just a compat hack · f2e41316
  Ralf Jung authored Feb 18, 2020
  
  f2e41316
17 Feb, 2020 1 commit
- direct future uploads at the appendix-3.3 · 564b7d5c
  Ralf Jung authored Feb 17, 2020
  
  564b7d5c
15 Feb, 2020 2 commits
- Merge branch 'fix-ignored-implicit-warning' into 'master' · 05b1c41f
  Ralf Jung authored Feb 15, 2020
```
Remove useless implicit annotation on binder

See merge request iris/iris!376
```
  05b1c41f
- Remove useless implicit annotation on binder · 144d62b0
  Tej Chajed authored Feb 15, 2020 and Ralf Jung committed Feb 15, 2020
```
Fixes a new warning on Coq 8.12+alpha when implicit annotations are used
in positions where they are ignored.
```
  144d62b0
14 Feb, 2020 5 commits
- Merge branch 'reflexive_transitive_closure' into 'master' · a3cea59c
  Robbert Krebbers authored Feb 14, 2020
```
Adding a constructor for reflexive transitive closures into bi's

See merge request iris/iris!375
```
  a3cea59c
- Adding a constructor for reflexive transitive closures into bi's · 3a6d86f4
  Jonas Kastberg authored Feb 14, 2020 and Robbert Krebbers committed Feb 14, 2020
  
  3a6d86f4
- Merge branch 'ralf/access' into 'master' · 22d31260
  Ralf Jung authored Feb 14, 2020
```
rename _open rules to _access if they are actually accessors

See merge request iris/iris!373
```
  22d31260
- changelog: list _acc renames · 357adad7
  Ralf Jung authored Feb 14, 2020
  
  357adad7
- mention Coq 8.11 in changelog · bc17fc9e
  Ralf Jung authored Feb 14, 2020
  
  bc17fc9e
13 Feb, 2020 1 commit
- play with CI config · 77852d7f
  Ralf Jung authored Feb 13, 2020
  
  77852d7f
12 Feb, 2020 2 commits
- stop timing Coq 8.9 · db3bebcd
  Ralf Jung authored Feb 12, 2020
  
  db3bebcd
- bump std++ · 3fc780ee
  Ralf Jung authored Feb 12, 2020
  
  3fc780ee
11 Feb, 2020 2 commits
- Write `twp_ind` in a more sane way. · 3c9e8424
  Robbert Krebbers authored Feb 11, 2020
  
  3c9e8424
- temporarily also time 8.9.1 again · e37a60a2
  Ralf Jung authored Feb 11, 2020
  
  e37a60a2