Commits · beb9d4458a293ac0642da2663a3c4dc2846d92e2 · Lennard Gäher / Iris

19 Feb, 2020 1 commit
- 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 6 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
- re-enable docs · 54e8c65f
  Ralf Jung authored Feb 11, 2020
  
  54e8c65f
- time on Coq 8.11 · 47372aaf
  Ralf Jung authored Feb 11, 2020
  
  47372aaf
- rename _access -> _acc · a8fe7b7f
  Ralf Jung authored Feb 11, 2020
  
  a8fe7b7f
- rename _open rules to _access if they are actually accessors · 1ff665fc
  Ralf Jung authored Feb 07, 2020
  
  1ff665fc
10 Feb, 2020 6 commits
- Merge branch 'twp_array' into 'master' · 0f2be668
  Robbert Krebbers authored Feb 10, 2020
```
Add twp_ lemmas for the arrays.

See merge request iris/iris!374
```
  0f2be668
- Merge branch 'ci/robbert/issue288' into 'master' · 511ed69b
  Robbert Krebbers authored Feb 10, 2020
```
Fix issue #288: iExists fails if goal after the existential quantifier is an evar

Closes #288

See merge request iris/iris!372
```
  511ed69b
- Disable test, since it's not compatible with Coq 8.8 and 8.9. · b6859ed1
  Robbert Krebbers authored Feb 10, 2020
  
  b6859ed1
- Add test case. · eef6260f
  Robbert Krebbers authored Feb 06, 2020
  
  eef6260f
- Fix issue #288. · c9c90cf6
  Robbert Krebbers authored Feb 06, 2020
  
  c9c90cf6
- Add twp_ lemmas for the arrays. · cc67112b
  Dan Frumin authored Feb 10, 2020
  
  cc67112b
07 Feb, 2020 1 commit

Merge branch 'ralf/cinv' into 'master' · 740affc3

Ralf Jung authored Feb 07, 2020

Linear invariant counterexample, and more cinv rules

Closes #132

See merge request iris/iris!368

740affc3