Merge branch 'robbert/hide_ipreprop' into 'master'
Put `iProp`/`iPreProp`-isomorphism into `own` construction See merge request iris/iris!530
No related branches found
No related tags found
Showing
- CHANGELOG.md 7 additions, 0 deletionsCHANGELOG.md
- theories/algebra/cmra.v 4 additions, 0 deletionstheories/algebra/cmra.v
- theories/algebra/updates.v 30 additions, 0 deletionstheories/algebra/updates.v
- theories/base_logic/bi.v 9 additions, 1 deletiontheories/base_logic/bi.v
- theories/base_logic/lib/boxes.v 4 additions, 6 deletionstheories/base_logic/lib/boxes.v
- theories/base_logic/lib/own.v 143 additions, 68 deletionstheories/base_logic/lib/own.v
- theories/base_logic/lib/saved_prop.v 3 additions, 9 deletionstheories/base_logic/lib/saved_prop.v
- theories/base_logic/lib/wsat.v 5 additions, 5 deletionstheories/base_logic/lib/wsat.v
- theories/base_logic/upred.v 9 additions, 1 deletiontheories/base_logic/upred.v
Loading
Please register or sign in to comment