Merge branch 'robbert/cleanup' into 'master'
Cleanup following the BI and SBI merge See merge request iris/iris!449
No related branches found
No related tags found
Showing
- _CoqProject 8 additions, 4 deletions_CoqProject
- theories/bi/bi.v 3 additions, 3 deletionstheories/bi/bi.v
- theories/bi/big_op.v 161 additions, 206 deletionstheories/bi/big_op.v
- theories/bi/derived_connectives.v 1 addition, 1 deletiontheories/bi/derived_connectives.v
- theories/bi/derived_laws.v 2 additions, 2 deletionstheories/bi/derived_laws.v
- theories/bi/derived_laws_later.v 5 additions, 4 deletionstheories/bi/derived_laws_later.v
- theories/bi/embedding.v 1 addition, 1 deletiontheories/bi/embedding.v
- theories/bi/interface.v 1 addition, 1 deletiontheories/bi/interface.v
- theories/bi/internal_eq.v 2 additions, 2 deletionstheories/bi/internal_eq.v
- theories/bi/lib/fractional.v 1 addition, 1 deletiontheories/bi/lib/fractional.v
- theories/bi/plainly.v 2 additions, 2 deletionstheories/bi/plainly.v
- theories/bi/updates.v 2 additions, 2 deletionstheories/bi/updates.v
- theories/proofmode/class_instances.v 7 additions, 209 deletionstheories/proofmode/class_instances.v
- theories/proofmode/class_instances_embedding.v 211 additions, 0 deletionstheories/proofmode/class_instances_embedding.v
- theories/proofmode/class_instances_internal_eq.v 50 additions, 0 deletionstheories/proofmode/class_instances_internal_eq.v
- theories/proofmode/class_instances_later.v 5 additions, 298 deletionstheories/proofmode/class_instances_later.v
- theories/proofmode/class_instances_plainly.v 101 additions, 0 deletionstheories/proofmode/class_instances_plainly.v
- theories/proofmode/class_instances_updates.v 182 additions, 0 deletionstheories/proofmode/class_instances_updates.v
- theories/proofmode/coq_tactics.v 66 additions, 73 deletionstheories/proofmode/coq_tactics.v
- theories/proofmode/tactics.v 4 additions, 1 deletiontheories/proofmode/tactics.v
Loading
Please register or sign in to comment