Commits · bdb7b828d31308397fd0161ad5f708dd457bfc3f · Glen Mével / Iris

13 Aug, 2019 7 commits
- Add test case. · bdb7b828
  Robbert Krebbers authored Aug 12, 2019
  
  bdb7b828
- Fix issue #260. · 890b60e5
  Robbert Krebbers authored Aug 12, 2019
  
  890b60e5
- Merge branch 'robbert/issue259' into 'master' · d6672184
  Robbert Krebbers authored Aug 13, 2019
```
Fix issue #259: Error message when iRevert is used on out of scope variable

Closes #259

See merge request iris/iris!301
```
  d6672184
- Add a bunch of test cases for `iRevert`. · 9b1cb055
  Robbert Krebbers authored Aug 12, 2019
  
  9b1cb055
- Improve error message of `iRevert` in case of used variable. · 9c43011e
  Robbert Krebbers authored Aug 13, 2019
  
  9c43011e
- Factor out anonymous rec in `iRevertIntros` to get cleaner Ltac backtraces. · 9a93c850
  Robbert Krebbers authored Aug 13, 2019
  
  9a93c850
- Fix issue #259. · b0c4d25c
  Robbert Krebbers authored Aug 12, 2019
```
Based on @Blaisorblade's suggestion.
```
  b0c4d25c
12 Aug, 2019 5 commits
- Merge branch 'ralf/discrete' into 'master' · 2dc1c367
  Robbert Krebbers authored Aug 12, 2019
```
fix typo in -d> docs

See merge request iris/iris!298
```
  2dc1c367
- fix typo in -d> docs · 345e24d7
  Ralf Jung authored Aug 12, 2019 and Robbert Krebbers committed Aug 12, 2019
  
  345e24d7
- comment examples · 74858b88
  Ralf Jung authored Aug 12, 2019
  
  74858b88
- Merge branch 'heap_lang_lib' into 'master' · 64f63272
  Robbert Krebbers authored Aug 12, 2019
```
Add some trivial but useful heaplang libraries.

See merge request iris/iris!291
```
  64f63272
- Add some trivial but useful heaplang libraries. · 3f9e2ea5
  Rodolphe Lepigre authored Aug 12, 2019 and Robbert Krebbers committed Aug 12, 2019
  
  3f9e2ea5
09 Aug, 2019 1 commit
- add one_shot_once example · 6c620a09
  Ralf Jung authored Aug 09, 2019
  
  6c620a09
08 Aug, 2019 4 commits
- Merge branch 'doc-style' into 'master' · 30d1385e
  Ralf Jung authored Aug 08, 2019
```
More conventions in style guide

See merge request iris/iris!297
```
  30d1385e
- Merge branch 'prop_ext_clearer' into 'master' · fe8938ea
  Ralf Jung authored Aug 08, 2019
```
Clearer statement for propositional extensionality

See merge request iris/iris!296
```
  fe8938ea
- Document more naming conventions · 96242aaf
  Paolo G. Giarrusso authored Aug 06, 2019
```
Examples for I and SI: uPredI, uPredSI, iPropI, iPropSI.
```
  96242aaf
- Clearer statement for propositional extensionality · 9312ad02
  Paolo G. Giarrusso authored Aug 06, 2019
```
- And use prop_ext instead of prop_ext_2 in other proofs.
```
  9312ad02
07 Aug, 2019 1 commit
- Rename prop_ext to prop_ext_2 · 69971a15
  Paolo G. Giarrusso authored Aug 08, 2019
  
  69971a15
06 Aug, 2019 1 commit
- Spelling fix · ad40ff4d
  Paolo G. Giarrusso authored Aug 06, 2019
  
  ad40ff4d
30 Jul, 2019 1 commit
- explain weird anonymous type field in CmraT · 625011cf
  Ralf Jung authored Jul 30, 2019
  
  625011cf
22 Jul, 2019 1 commit
- mention how to use iLöb for recursive functions · 8dfda06c
  Ralf Jung authored Jul 22, 2019
  
  8dfda06c
14 Jul, 2019 4 commits
- Merge branch 'big_sepL2_app_inv_2' into 'master' · 0cdad2cb
  Robbert Krebbers authored Jul 14, 2019
```
Add `big_sepL2_app_inv_2`.

See merge request iris/iris!292
```
  0cdad2cb
- Rename `big_sepL2_app_inv_2` -> `big_sepL2_app_inv`. · 2a4e4330
  Dan Frumin authored Jul 14, 2019 and Robbert Krebbers committed Jul 14, 2019
```
And shorten the proof.
```
  2a4e4330
- Merge branch 'head_prim_fill_reducible' into 'master' · cd8f3be9
  Robbert Krebbers authored Jul 14, 2019
```
Add `head_prim_fill_reducible`.

See merge request iris/iris!293
```
  cd8f3be9
- Add `head_prim_fill_reducible`. · 4767c8f9
  Dan Frumin authored Jul 14, 2019 and Robbert Krebbers committed Jul 14, 2019
```
A more general implication from `head_reducible` to `reducible`.
```
  4767c8f9
13 Jul, 2019 7 commits
- Merge branch 'sigTO_proper_projs' into 'master' · 9b77b750
  Robbert Krebbers authored Jul 13, 2019
```
Mark projections for sigTO as NonExpansive and Proper

See merge request iris/iris!285
```
  9b77b750
- Mark projections for sigTO as NonExpansive and Proper · 53a18cf8
  Paolo G. Giarrusso authored Jul 13, 2019 and Robbert Krebbers committed Jul 13, 2019
  
  53a18cf8
- proper link and less Rust ;) · 94533e33
  Ralf Jung authored Jul 13, 2019
  
  94533e33
- erasure is in iris/examples · b5e2eb4e
  Ralf Jung authored Jul 13, 2019
  
  b5e2eb4e
- Weaken premise of `gmultiset_local_update_dealloc`. · 736b17dc
  Robbert Krebbers authored Jul 13, 2019
  
  736b17dc
- Merge branch 'ralf/pair-core' into 'master' · 8f41613d
  Robbert Krebbers authored Jul 13, 2019
```
show that pair construction commutes with taking the core

See merge request iris/iris!286
```
  8f41613d
- shorten proof · 162755de
  Ralf Jung authored Jul 13, 2019
  
  162755de
12 Jul, 2019 2 commits
- tweak proof to also work after a Coq bugfix · e6f6758c
  Ralf Jung authored Jul 12, 2019
  
  e6f6758c
- changelog for comparison changes · f455b5d4
  Ralf Jung authored Jul 12, 2019
  
  f455b5d4
09 Jul, 2019 4 commits
- dont quantify over empty telescopes · c2eaa77d
  Ralf Jung authored Jul 09, 2019
  
  c2eaa77d
- Merge branch 'fresh_locs_arg' into 'master' · 64c16f99
  Robbert Krebbers authored Jul 09, 2019
```
Get rid of a superflous argument to `fresh_locs`.

See merge request iris/iris!288
```
  64c16f99
- Get rid of a superflous argument to `fresh_locs`. · 80623a8c
  Dan Frumin authored Jul 09, 2019
  
  80623a8c
- bump std++ · 5123ac6b
  Ralf Jung authored Jul 09, 2019
  
  5123ac6b
07 Jul, 2019 1 commit
- show that pair cosntruction commutes with taking the core · c2d34fe3
  Ralf Jung authored Jul 07, 2019
  
  c2d34fe3
05 Jul, 2019 1 commit
- Bump stdpp. · 4a624063
  Robbert Krebbers authored Jul 05, 2019
  
  4a624063