Merge branch 'ralf/dependency-stratification' into 'master'
remove algebra/ dependency on base_logic/ Closes #355 See merge request iris/iris!549
Showing
- CHANGELOG.md 7 additions, 0 deletionsCHANGELOG.md
- _CoqProject 1 addition, 0 deletions_CoqProject
- theories/algebra/agree.v 1 addition, 14 deletionstheories/algebra/agree.v
- theories/algebra/auth.v 1 addition, 25 deletionstheories/algebra/auth.v
- theories/algebra/csum.v 4 additions, 25 deletionstheories/algebra/csum.v
- theories/algebra/excl.v 1 addition, 15 deletionstheories/algebra/excl.v
- theories/algebra/gmap.v 3 additions, 38 deletionstheories/algebra/gmap.v
- theories/algebra/lib/excl_auth.v 0 additions, 8 deletionstheories/algebra/lib/excl_auth.v
- theories/algebra/lib/gmap_view.v 0 additions, 21 deletionstheories/algebra/lib/gmap_view.v
- theories/algebra/list.v 3 additions, 26 deletionstheories/algebra/list.v
- theories/algebra/proofmode_classes.v 0 additions, 1 deletiontheories/algebra/proofmode_classes.v
- theories/algebra/view.v 2 additions, 60 deletionstheories/algebra/view.v
- theories/base_logic/algebra.v 258 additions, 0 deletionstheories/base_logic/algebra.v
- theories/base_logic/base_logic.v 1 addition, 1 deletiontheories/base_logic/base_logic.v
- theories/base_logic/bi.v 0 additions, 7 deletionstheories/base_logic/bi.v
- theories/base_logic/lib/own.v 1 addition, 0 deletionstheories/base_logic/lib/own.v
- theories/base_logic/proofmode.v 1 addition, 0 deletionstheories/base_logic/proofmode.v
- theories/base_logic/upred.v 0 additions, 9 deletionstheories/base_logic/upred.v
- theories/bi/big_op.v 38 additions, 1 deletiontheories/bi/big_op.v
Loading
Please register or sign in to comment