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
add iSplitWith tactic for convenient conjunction monotonicity

!141 · created Apr 23, 2018 by Ralf Jung gen_proofmode T-proofmode
- CLOSED
- 1
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
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
Consistent handling of pure implication and forall

!104 · created Dec 20, 2017 by Robbert Krebbers T-proofmode
- MERGED
- 6
updated Dec 21, 2017
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
Factor plainly out of main BI interface

!98 · created Dec 06, 2017 by Ralf Jung Generalized Proofmode Merger gen_proofmode T-proofmode
- CLOSED
- 171
updated Mar 03, 2018
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
WIP: Strong framing

!50 · created Feb 18, 2017 by Robbert Krebbers T-proofmode
- CLOSED
- 31
updated Nov 01, 2019
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