Commits · master · Gregory Malecha / Iris

16 Jan, 2020 2 commits
- Merge branch 'seal_big_opM' into 'master' · 463f24ef
  Robbert Krebbers authored Jan 16, 2020
```
Seal big_sepM2

See merge request iris/iris!352
```
  463f24ef
- seal big_opM, big_opS, big_opMS and big_sepM2 · bdaec8c5
  Michael Sammler authored Dec 27, 2019
  
  bdaec8c5
15 Jan, 2020 4 commits
- Bump std++. · d6c5699b
  Robbert Krebbers authored Jan 15, 2020
  
  d6c5699b
- Merge branch 'robbert/from_forall_tc_opaque' into 'master' · 23ad2f43
  Robbert Krebbers authored Jan 15, 2020
```
Missing `tc_opaque` instance for `FromForall`.

See merge request iris/iris!357
```
  23ad2f43
- Add test. · 2c980e72
  Robbert Krebbers authored Jan 15, 2020
  
  2c980e72
- Missing `tc_opaque` instance for `FromForall`. · a42f1b54
  Robbert Krebbers authored Jan 15, 2020
  
  a42f1b54
14 Jan, 2020 2 commits
- time coq master again · 352c5d42
  Ralf Jung authored Jan 14, 2020
  
  352c5d42
- Merge branch 'robbert/sprop' into 'master' · ffd67b21
  Robbert Krebbers authored Jan 14, 2020
```
Step-indexed propositions

See merge request iris/iris!304
```
  ffd67b21
13 Jan, 2020 11 commits
- Add some basic tests for the `siProp` proofmode. · 9714dfdb
  Robbert Krebbers authored Jan 13, 2020
  
  9714dfdb
- CHANGELOG entry. · ae859c84
  Robbert Krebbers authored Jan 13, 2020
  
  ae859c84
- Add some documentation. · ed34db95
  Robbert Krebbers authored Jan 13, 2020
  
  ed34db95
- BI instances for `siProp`. · f661622b
  Robbert Krebbers authored Dec 06, 2019
  
  f661622b
- Type `siProp` for "plain" step-indexed propositions. · 20996da6
  Robbert Krebbers authored Aug 16, 2019
  
  20996da6
- fix README for real · 55aef759
  Ralf Jung authored Jan 13, 2020
  
  55aef759
- fix README · 204c673c
  Ralf Jung authored Jan 13, 2020
  
  204c673c
- use https URL · 5b6dd1fd
  Ralf Jung authored Jan 13, 2020
  
  5b6dd1fd
- disable docs building again, it still does not work · db614d95
  Ralf Jung authored Jan 13, 2020
  
  db614d95
- fix opam file a bit more · fde6c215
  Ralf Jung authored Jan 13, 2020
  
  fde6c215
- upgrade opam file to opam 2 · 4fc1ca8b
  Ralf Jung authored Jan 13, 2020
  
  4fc1ca8b
11 Jan, 2020 1 commit
- Merge branch 'fix-instance-name' into 'master' · 1d977b49
  Robbert Krebbers authored Jan 11, 2020
```
Rename Awesome_{ne,proper} to NamespaceMap_{ne,proper}

See merge request iris/iris!356
```
  1d977b49
10 Jan, 2020 3 commits
- docs publishing should work again · 7dc625d0
  Ralf Jung authored Jan 10, 2020
  
  7dc625d0
- disable doc publishing until we sort out the SSH situation · 48b47dc0
  Ralf Jung authored Jan 10, 2020
  
  48b47dc0
- re-enable coq.dev build · 567abf3d
  Ralf Jung authored Jan 10, 2020
  
  567abf3d
09 Jan, 2020 6 commits
- Merge branch 'ralf/own-alloc-dep' into 'master' · 1142d94c
  Ralf Jung authored Jan 09, 2020
```
add dependent allocation lemma to own

See merge request iris/iris!354
```
  1142d94c
- disable coq.dev build for now · 1fcb9286
  Ralf Jung authored Jan 09, 2020
```
The build is broken, see https://github.com/coq/coq/issues/11383
```
  1fcb9286
- adjust atomic test for more Coq compatibility · 97b83157
  Ralf Jung authored Jan 09, 2020
  
  97b83157
- Merge branch 'ralf/awp_apply' into 'master' · 7d9882cd
  Ralf Jung authored Jan 09, 2020
```
Fix and test `awp_apply` error message, and also use `tactic3` everywhere

See merge request iris/iris!355
```
  7d9882cd
- Merge branch 'jh/lanzy_andb' into 'master' · 00261263
  Robbert Krebbers authored Jan 09, 2020
```
Use &&& from lazy_bool_scope instead of redefining the && notation.

See merge request iris/iris!349
```
  00261263
- fix the last remaining tactic() · 4d52d195
  Ralf Jung authored Jan 09, 2020
  
  4d52d195
08 Jan, 2020 4 commits
- fix ltac parsing · a8054b66
  Ralf Jung authored Jan 08, 2020
  
  a8054b66
- fix awp_apply error message · d3556db2
  Ralf Jung authored Jan 08, 2020
  
  d3556db2
- add test for iAuIntro errors (status quo) · 1f9c5efc
  Ralf Jung authored Jan 08, 2020
  
  1f9c5efc
- save some lines and organize · 1d2149cc
  Ralf Jung authored Jan 08, 2020
  
  1d2149cc
07 Jan, 2020 4 commits
- strengthen alloc_updateP_strong_dep and own_alloc_strong_dep · 11148461
  Ralf Jung authored Jan 07, 2020
  
  11148461
- unicode · 8e7e3982
  Ralf Jung authored Jan 07, 2020
  
  8e7e3982
- add dependent allocation lemma to own · 96882993
  Ralf Jung authored Jan 07, 2020
  
  96882993
- Rename Awesome_{ne,proper} to NamespaceMap_{ne,proper} · 38df0d21
  Paolo G. Giarrusso authored Jan 07, 2020
  
  38df0d21
20 Dec, 2019 2 commits
- Merge branch 'big_sepM2_fmap_fix' into 'master' · 62798412
  Ralf Jung authored Dec 20, 2019
```
fix big_sepM2_fmap and friend to work for keys other than nat

Closes #283

See merge request iris/iris!351
```
  62798412
- fix big_sepM2_fmap and friend to work for keys other than nat · 8d0e35d6
  Michael Sammler authored Dec 20, 2019
  
  8d0e35d6
19 Dec, 2019 1 commit
- Merge branch 'fix-doc-links' into 'master' · 247428ee
  Ralf Jung authored Dec 19, 2019
```
[doc] Fix links to doc files

Closes #281

See merge request iris/iris!350
```
  247428ee