Merge branch 'ralf/proofmode-emp' into 'master'
proofmode: do not treat pure assertions as persistent See merge request iris/iris!799
No related branches found
No related tags found
Showing
- CHANGELOG.md 5 additions, 0 deletionsCHANGELOG.md
- iris/bi/derived_laws.v 7 additions, 0 deletionsiris/bi/derived_laws.v
- iris/proofmode/class_instances.v 34 additions, 15 deletionsiris/proofmode/class_instances.v
- iris/proofmode/coq_tactics.v 5 additions, 5 deletionsiris/proofmode/coq_tactics.v
- iris/proofmode/ltac_tactics.v 1 addition, 1 deletioniris/proofmode/ltac_tactics.v
- tests/proofmode.ref 44 additions, 0 deletionstests/proofmode.ref
- tests/proofmode.v 53 additions, 0 deletionstests/proofmode.v
Loading
Please register or sign in to comment