Merge requests · Iris / Iris · GitLab

Make iDestruct consume wands when it's supposed to

!591 · created Nov 25, 2020 by Tej Chajed T-proofmode
- MERGED
- 16
updated Dec 04, 2020
Remove plainly_exist_1 from the BI axioms.

!95 · created Dec 04, 2017 by Jacques-Henri Jourdan gen_proofmode T-proofmode
- MERGED
- 21
updated Jul 13, 2018
Proof mode support for monotonous predicates.

!100 · created Dec 11, 2017 by Jacques-Henri Jourdan janno/monfun T-proofmode
- MERGED
- 53
updated Jul 13, 2018
Make `FromPure` depend on an affinity parameter

!114 · created Feb 12, 2018 by Jacques-Henri Jourdan gen_proofmode T-proofmode
- MERGED
- 4
updated Jul 13, 2018
rename affinely_persistently -> intuitionistically; and make it a TC-opaque definition

!130 · created Mar 19, 2018 by Ralf Jung Generalized Proofmode Merger gen_proofmode T-proofmode
- MERGED
- 28
updated Mar 22, 2018
Set mode for update modalities

!115 · created Feb 13, 2018 by Ralf Jung gen_proofmode T-proofmode
- MERGED
- 32
updated Feb 14, 2018
Consistent handling of pure implication and forall

!104 · created Dec 20, 2017 by Robbert Krebbers T-proofmode
- MERGED
- 6
updated Dec 21, 2017
ProofMode intro patterns: accept _ as part of variable names

!29 · created Nov 24, 2016 by Ralf Jung T-proofmode
- MERGED
- 1
updated Nov 24, 2016