Issues · Iris / Iris

New issue

iDestruct and iPureIntro

#21 · opened Jul 27, 2016 by Ghost User A-coq C-enhancement T-proofmode
- CLOSED
- 3
updated Nov 01, 2019
Ticket lock proof

#22 · opened Aug 01, 2016 by Ghost User
- CLOSED
- 0
updated Aug 02, 2016
iFrame should support conjunction

#23 · opened Aug 02, 2016 by Ghost User
- CLOSED
- 8
updated Aug 02, 2016
Find nice syntax for our "CPS" WP specifications

#24 · opened Aug 05, 2016 by Ralf Jung
- CLOSED
- 2
updated Oct 27, 2016
iSplitL "persistent_hyp": Improve error

#25 · opened Aug 05, 2016 by Ralf Jung T-proofmode
- CLOSED
- 0
updated Aug 06, 2016
heap-lang CAS capability

#26 · opened Aug 08, 2016 by Ghost User
- CLOSED
- 14
updated Oct 21, 2016
mathpartir.sty is missing

#27 · opened Aug 09, 2016 by Jeehoon Kang
- CLOSED
- 3
updated Aug 09, 2016
docs: the universe $\cal U$ is used without definition

#28 · opened Aug 14, 2016 by Jeehoon Kang
- CLOSED
- 0
updated Aug 16, 2016
Bring back Logically Atomic Triples (Coq + docs) 1 of 2 tasks completed

#29 · opened Aug 16, 2016 by Jeehoon Kang A-theory C-project T-logical-atomicity
- 7
updated Nov 01, 2019
Make coqchk (make verify) work

#30 · opened Aug 19, 2016 by Ralf Jung
- CLOSED
- 5
updated Aug 19, 2016
iMod doesn't handle mismatched mask

#31 · opened Aug 23, 2016 by Ghost User A-coq C-enhancement T-proofmode
- 1
- 20
updated Oct 02, 2020
Support framing pure/Coq hypotheses

#32 · opened Sep 05, 2016 by Jacques-Henri Jourdan
- CLOSED
- 5
updated Sep 19, 2016
Confusing error msg for `iTimeless`

#33 · opened Sep 12, 2016 by Ghost User T-proofmode
- CLOSED
- 10
updated Oct 27, 2016
Coq induction support in proof mode

#34 · opened Sep 12, 2016 by Jacques-Henri Jourdan
- CLOSED
- 7
updated Sep 30, 2016
Renaming things

#35 · opened Sep 29, 2016 by Ralf Jung Iris 3.0
- CLOSED
- 42
updated Nov 09, 2016
STSs: Consider changing the def. of frame-steps

#36 · opened Sep 29, 2016 by Ralf Jung A-theory C-project T-algebra
- CLOSED
- 5
updated Nov 01, 2019
saved_prop for predicate

#37 · opened Oct 05, 2016 by Ghost User
- CLOSED
- 8
updated Oct 05, 2016
Refactor bigops

#38 · opened Oct 10, 2016 by Ralf Jung
- CLOSED
- 1
- 4
updated Apr 01, 2017
iIntros: bad error when trying to use a name that's already used

#39 · opened Oct 26, 2016 by Ralf Jung T-proofmode
- CLOSED
- 1
updated Oct 26, 2016
iRewrite and internal equality on predicates

#40 · opened Oct 27, 2016 by Janno
- CLOSED
- 4
updated Oct 27, 2016