Issues · Iris / Iris

New issue

iDestruct and iPureIntro

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

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

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

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

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

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

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

#28 · created 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 · created Aug 16, 2016 by Jeehoon Kang A-theory C-project T-logical-atomicity
- 7
updated Nov 01, 2019
Make coqchk (make verify) work

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

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

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

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

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

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

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

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

#38 · created 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 · created Oct 26, 2016 by Ralf Jung T-proofmode
- CLOSED
- 1
updated Oct 26, 2016
iRewrite and internal equality on predicates

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