Issues · Iris / Iris

New issue

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

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

#108 · opened 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 · opened 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 · opened 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 · opened 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 · opened Sep 29, 2017 by Ralf Jung Iris 3.1 T-proofmode
- CLOSED
- 15
updated Nov 11, 2017
Let iAlways clear the spatial context

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

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

#56 · opened 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 · opened 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 · opened Dec 19, 2016 by Ralf Jung Iris 3.0 T-proofmode
- CLOSED
- 3
updated Dec 21, 2016
iMod and evar instantiation

#52 · opened 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 · opened Dec 14, 2016 by Ralf Jung Iris 3.0
- CLOSED
- 42
updated Jan 14, 2017
Use opam-based CI

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

#35 · opened Sep 29, 2016 by Ralf Jung Iris 3.0
- CLOSED
- 42
updated Nov 09, 2016
wp_bind does not report a failure message

#401 · opened Feb 02, 2021 by Tej Chajed
- CLOSED
- 1
- 0
updated Feb 02, 2021
fupd_plainly_laterN = fupd_plain_laterN ?

#393 · opened Dec 23, 2020 by Paolo G. Giarrusso
- CLOSED
- 1
- 1
updated Dec 23, 2020
Dropping support for Coq 8.10

#388 · opened Dec 04, 2020 by Tej Chajed A-coq
- CLOSED
- 1
- 1
- 2
updated Dec 16, 2020
Deprecate unqualified "Instance"

#387 · opened Dec 03, 2020 by Ralf Jung A-coq C-enhancement T-style
- CLOSED
- 4
updated Dec 19, 2020
Quote does not handle ⊣⊢

#373 · opened Nov 03, 2020 by Rodolphe Lepigre
- CLOSED
- 1
updated Nov 05, 2020