Commits · 9bdda372aa71861ddce2bfccdb127a31fa147fcd · Iris / Iris

04 Apr, 2018 4 commits
- Merge branch 'gen_proofmode' of gitlab.mpi-sws.org:FP/iris-coq into gen_proofmode · 9bdda372
  Robbert Krebbers authored Apr 04, 2018
  
  9bdda372
- Merge branch 'master' into gen_proofmode · a0d93e84
  Robbert Krebbers authored Apr 04, 2018
  
  a0d93e84
- update CI · 6f122df4
  Ralf Jung authored Apr 04, 2018
  
  6f122df4
- Fix some bad names. · b8938010
  Robbert Krebbers authored Apr 03, 2018
  
  b8938010
03 Apr, 2018 7 commits
- Slightly more easy to use version of strong `inv_open`. · 23178b78
  Robbert Krebbers authored Apr 03, 2018
```
The closing view shift's LHS mask is now universally quantified, which
makes it easier to execute the closing view shift.
```
  23178b78
- Stronger version of `inv_open` that allows to close invariants in a different order. · 5e7d9ca7
  Robbert Krebbers authored Apr 03, 2018
  
  5e7d9ca7
- update CI · 7143c8b7
  Ralf Jung authored Apr 03, 2018
  
  7143c8b7
- Merge branch 'ralf/lemma_rename' into 'gen_proofmode' · 9d68507d
  Ralf Jung authored Apr 03, 2018
```
more consistent lemma naming

See merge request FP/iris-coq!135
```
  9d68507d
- fix gitlab-extract output if build is still running · 542323df
  Ralf Jung authored Apr 03, 2018
  
  542323df
- update CI · b6d91cd4
  Ralf Jung authored Apr 03, 2018
  
  b6d91cd4
- stop adding the quick2vo target · fdd199fb
  Ralf Jung authored Apr 03, 2018
  
  fdd199fb
31 Mar, 2018 1 commit
- update CI · 8cfc4e2c
  Ralf Jung authored Mar 31, 2018
  
  8cfc4e2c
28 Mar, 2018 1 commit
- Fix typos. · fb1221c5
  Robbert Krebbers authored Mar 28, 2018
  
  fb1221c5
27 Mar, 2018 1 commit
- Short proof of `big_sepL_delete`. · 3bc1f853
  Robbert Krebbers authored Mar 27, 2018
```
This is a substitute for !136.
```
  3bc1f853
24 Mar, 2018 13 commits
- update CI · c403f3cd
  Ralf Jung authored Mar 24, 2018
  
  c403f3cd
- Merge remote-tracking branch 'origin/master' into gen_proofmode · ebbe0df0
  Ralf Jung authored Mar 24, 2018
  
  ebbe0df0
- update CI · 88d2204f
  Ralf Jung authored Mar 24, 2018
  
  88d2204f
- update CI: use centralized CI repo; submiting timing to coq-speed · f5854570
  Ralf Jung authored Mar 24, 2018
  
  f5854570
- gitlab-extract: show which commit the bad line was in · 658c756f
  Ralf Jung authored Mar 24, 2018
  
  658c756f
- update CI · f2b0a849
  Ralf Jung authored Mar 24, 2018
  
  f2b0a849
- update CI · 67f3284b
  Ralf Jung authored Mar 24, 2018
  
  67f3284b
- gitlab-extract: add support for excluding a branch · 7eb3534d
  Ralf Jung authored Mar 24, 2018
  
  7eb3534d
- update CI · a5f0e7d8
  Ralf Jung authored Mar 24, 2018
  
  a5f0e7d8
- we can't use variables in 'only:', so go back to OPAM_PKG_BRANCH · 812e9c44
  Ralf Jung authored Mar 24, 2018
  
  812e9c44
- update CI: use dedicated buildjob script, submit timing information to coq-speed · 2cc7b4d8
  Ralf Jung authored Mar 24, 2018
  
  2cc7b4d8
- CI needs submodules now · 5361ad82
  Ralf Jung authored Mar 24, 2018
  
  5361ad82
- move CI scripts to submodule · a44b4c8c
  Ralf Jung authored Mar 24, 2018
  
  a44b4c8c
22 Mar, 2018 3 commits
- Merge remote-tracking branch 'origin/master' into gen_proofmode · fe155b62
  Ralf Jung authored Mar 22, 2018
  
  fe155b62
- more consistent lemma naming · 0c4a3e1b
  Ralf Jung authored Mar 22, 2018
```
Fixes #177
```
  0c4a3e1b
- CI: test Coq 8.8 branch · 9ca430f6
  Ralf Jung authored Mar 22, 2018
  
  9ca430f6
21 Mar, 2018 9 commits
- verified compatibility with Coq 8.8 (CI coming later) · 7b0ad6cd
  Ralf Jung authored Mar 21, 2018
  
  7b0ad6cd
- bump std++; no changes needed · 8ab26a68
  Ralf Jung authored Mar 21, 2018
  
  8ab26a68
- Stop iFrame from introducing modalities · bcce68db
  Ralf Jung authored Mar 21, 2018
```
Fixes #176
```
  bcce68db
- move Frame instances to their own file · 458a6d45
  Ralf Jung authored Mar 21, 2018
  
  458a6d45
- split class_instances into BI and SBI instanced · 528b255f
  Ralf Jung authored Mar 21, 2018
  
  528b255f
- split derived_laws into BI and SBI laws · dfc4dca9
  Ralf Jung authored Mar 21, 2018
  
  dfc4dca9
- move general BI things using the proofmode down into lib/ · c2a8bce0
  Ralf Jung authored Mar 21, 2018
  
  c2a8bce0
- Merge branch 'ralf/intuitionistically' into 'gen_proofmode' · ef2adeb3
  Ralf Jung authored Mar 21, 2018
```
rename affinely_persistently -> intuitionistically; and make it a TC-opaque definition

See merge request FP/iris-coq!130
```
  ef2adeb3
- apply Robbert's feedback · ff398120
  Ralf Jung authored Mar 21, 2018
  
  ff398120
20 Mar, 2018 1 commit
- FromAffinely instance for intuitionistic modality · 861490f0
  Ralf Jung authored Mar 20, 2018
  
  861490f0