Merge branch 'ralf/bi_disambig' into 'gen_proofmode'
add notation to define the PROP we use for a particular turnstile See merge request FP/iris-coq!134
No related branches found
No related tags found
Showing
- theories/bi/big_op.v 1 addition, 1 deletiontheories/bi/big_op.v
- theories/bi/derived_laws_bi.v 8 additions, 8 deletionstheories/bi/derived_laws_bi.v
- theories/bi/derived_laws_sbi.v 9 additions, 9 deletionstheories/bi/derived_laws_sbi.v
- theories/bi/embedding.v 3 additions, 3 deletionstheories/bi/embedding.v
- theories/bi/interface.v 19 additions, 9 deletionstheories/bi/interface.v
- theories/bi/monpred.v 1 addition, 1 deletiontheories/bi/monpred.v
- theories/bi/plainly.v 7 additions, 7 deletionstheories/bi/plainly.v
- theories/proofmode/class_instances_sbi.v 1 addition, 1 deletiontheories/proofmode/class_instances_sbi.v
Loading
Please register or sign in to comment