Issues · Iris / Iris

New issue

Proof mode only *mostly* works when it is transitively imported, not exported

#111 · created Nov 16, 2017 by Ralf Jung Iris 3.1 T-proofmode
- CLOSED
- 7
updated Nov 20, 2017
iIntros on pure implications stopped working

#108 · created Oct 28, 2017 by Ralf Jung Iris 3.1 T-proofmode
- CLOSED
- 7
updated Oct 28, 2017
Reverting to old (stronger) definition of atomicity

#107 · created Oct 27, 2017 by Amin Timany Iris 3.1
- CLOSED
- 1
- 17
updated Oct 29, 2017
Iris 3.1 3 of 4 tasks completed

#106 · created Oct 27, 2017 by Ralf Jung Iris 3.1
- CLOSED
- 8
updated Jan 09, 2018
Add some theory about the interaction of plainly and fancy updates

#105 · created Oct 27, 2017 by Ralf Jung Iris 3.1
- CLOSED
- 1
- 2
updated Nov 01, 2017
Proof mode notation broken depending on import order

#100 · created Sep 29, 2017 by Ralf Jung Iris 3.1 T-proofmode
- CLOSED
- 15
updated Nov 11, 2017
Let iAlways clear the spatial context

#81 · created Mar 16, 2017 by Ralf Jung Iris 3.1 T-proofmode
- CLOSED
- 16
updated Oct 27, 2017
Stronger Invariant Allocation Rules

#59 · created Dec 29, 2016 by Janno Iris 3.0
- CLOSED
- 9
updated Jan 11, 2017
iAssert ... as %X should get all assumptions

#56 · created Dec 20, 2016 by Ralf Jung Iris 3.0 T-proofmode
- CLOSED
- 1
updated Jan 03, 2017
iNext unfolds things (more than simpl) even when there is no later to strip

#55 · created Dec 20, 2016 by Ralf Jung Iris 3.0 T-proofmode
- CLOSED
- 10
updated Feb 20, 2018
iIntros fails to introduce Coq-level and Iris-level universal quantifiers at once

#54 · created Dec 19, 2016 by Ralf Jung Iris 3.0 T-proofmode
- CLOSED
- 3
updated Dec 21, 2016
iMod and evar instantiation

#52 · created Dec 19, 2016 by Ralf Jung Iris 3.0 T-proofmode
- CLOSED
- 4
updated Jun 17, 2019
`contains` is named the wrong way around

#50 · created Dec 14, 2016 by Ralf Jung Iris 3.0
- CLOSED
- 42
updated Jan 14, 2017
Use opam-based CI

#47 · created Nov 30, 2016 by Ralf Jung Iris 3.0
- CLOSED
- 2
updated Dec 14, 2016
Renaming things

#35 · created Sep 29, 2016 by Ralf Jung Iris 3.0
- CLOSED
- 42
updated Nov 09, 2016
Typo in documentation

#437 · created Oct 19, 2021 by Alexandre Moine
- CLOSED
- 1
updated Oct 26, 2021
opam package description is not helpful

#436 · created Oct 18, 2021 by Michael Soegtrop
- CLOSED
- 1
- 3
updated Oct 26, 2021
iApply "auto frame": bad error message

#432 · created Sep 01, 2021 by Ralf Jung
- CLOSED
- 1
- 0
updated Sep 06, 2021
Bad error message for failing iInduction

#421 · created Jun 08, 2021 by Ralf Jung A-coq C-bug T-proofmode
- CLOSED
- 1
- 1
updated Jun 14, 2021
Proposed change to naming convention for "dataful" `*G`s

#409 · created Mar 18, 2021 by Ralf Jung A-coq C-enhancement T-style
- CLOSED
- 1
- 8
updated Jun 03, 2021