Merge branch 'robbert/bundle_bi_classes' into 'gen_proofmode'
Bundle classes for updates, plainly and embeddings See merge request FP/iris-coq!125
No related branches found
No related tags found
Showing
- _CoqProject 1 addition, 0 deletions_CoqProject
- theories/base_logic/derived.v 2 additions, 5 deletionstheories/base_logic/derived.v
- theories/base_logic/lib/fancy_updates.v 17 additions, 9 deletionstheories/base_logic/lib/fancy_updates.v
- theories/base_logic/upred.v 87 additions, 74 deletionstheories/base_logic/upred.v
- theories/bi/bi.v 2 additions, 2 deletionstheories/bi/bi.v
- theories/bi/big_op.v 73 additions, 55 deletionstheories/bi/big_op.v
- theories/bi/derived_connectives.v 0 additions, 22 deletionstheories/bi/derived_connectives.v
- theories/bi/derived_laws.v 3 additions, 500 deletionstheories/bi/derived_laws.v
- theories/bi/embedding.v 157 additions, 109 deletionstheories/bi/embedding.v
- theories/bi/interface.v 13 additions, 72 deletionstheories/bi/interface.v
- theories/bi/lib/atomic.v 3 additions, 3 deletionstheories/bi/lib/atomic.v
- theories/bi/monpred.v 198 additions, 145 deletionstheories/bi/monpred.v
- theories/bi/plainly.v 528 additions, 0 deletionstheories/bi/plainly.v
- theories/bi/updates.v 111 additions, 56 deletionstheories/bi/updates.v
- theories/proofmode/class_instances.v 193 additions, 206 deletionstheories/proofmode/class_instances.v
- theories/proofmode/classes.v 2 additions, 1 deletiontheories/proofmode/classes.v
- theories/proofmode/modality_instances.v 14 additions, 25 deletionstheories/proofmode/modality_instances.v
- theories/proofmode/monpred.v 59 additions, 54 deletionstheories/proofmode/monpred.v
- theories/proofmode/tactics.v 1 addition, 1 deletiontheories/proofmode/tactics.v
- theories/tests/proofmode_monpred.v 4 additions, 11 deletionstheories/tests/proofmode_monpred.v
Loading
Please register or sign in to comment