Issues · Iris / Iris

New issue

Regression after !329 on recursive proofs

#274 · created Nov 21, 2019 by Paolo G. Giarrusso A-coq C-bug T-proofmode
- CLOSED
- 1
- 0
updated Dec 02, 2019
Follow-up from "Lang lemmas": intuitive explanation of mixin_step_by_val

#271 · created Nov 06, 2019 by Ralf Jung Iris 3.3 A-theory C-enhancement T-heap_lang
- CLOSED
- 1
- 0
updated May 13, 2020
non-Unicode Iris notations

#270 · created Nov 01, 2019 by Ralf Jung A-coq C-enhancement T-style
- CLOSED
- 1
- 27
updated Apr 07, 2020
Editor config should explain how to configure CoqIDE 8.10 unicode input

#269 · created Oct 19, 2019 by Tej Chajed A-docs C-enhancement
- CLOSED
- 1
- 1
updated Feb 10, 2020
`iDestruct 1` does not work when `Z_scope` is open

#266 · created Sep 20, 2019 by Jacques-Henri Jourdan
- CLOSED
- 8
updated Sep 20, 2019
Add an "iStopProof" tactic

#265 · created Sep 06, 2019 by Jonas Kastberg
- CLOSED
- 1
- 0
updated Sep 11, 2019
IPM/MoSeL nested disjunction syntax

#263 · created Aug 29, 2019 by Dan Frumin
- CLOSED
- 2
updated Nov 01, 2019
Confusing error message if iLoeb is not available (non-step indexed BI)

#260 · created Aug 09, 2019 by Dan Frumin
- CLOSED
- 1
- 4
updated Aug 13, 2019
Confusing error message from iLoeb: `Variable x should be bound to a term but is bound to a ident.`

#259 · created Aug 09, 2019 by Dan Frumin
- CLOSED
- 1
- 1
updated Aug 13, 2019
Stronger `list_core_id`

#258 · created Aug 06, 2019 by Dmitry Khalanskiy A-coq C-enhancement Good First Issue T-algebra
- CLOSED
- 6
updated Mar 18, 2020
Auth as Views 0 of 2 tasks completed

#257 · created Aug 01, 2019 by Ralf Jung A-theory C-project T-algebra
- CLOSED
- 1
- 1
updated Oct 01, 2020
Consisent direction for `CMRA_NAME_op` lemmas.

#256 · created Jul 20, 2019 by Dan Frumin
- CLOSED
- 2
- 1
- 5
updated Aug 13, 2019
Failure to find a proof of persistence

#255 · created Jul 19, 2019 by Dmitry Khalanskiy A-coq C-bug S-blocked-by-coq T-algebra
- CLOSED
- 1
- 12
updated Mar 18, 2020
Reliance on `Export` bug

#254 · created Jul 09, 2019 by Maxime Dénès
- CLOSED
- 5
updated Nov 01, 2019
Constructing CMRAs by giving isomorphism to CMRAs

#253 · created Jul 09, 2019 by Paolo G. Giarrusso A-coq C-enhancement Good First Issue T-algebra
- CLOSED
- 1
- 1
- 5
updated Nov 06, 2020
equivI lemma for sigT

#250 · created Jun 24, 2019 by Paolo G. Giarrusso
- CLOSED
- 1
- 4
updated Jun 25, 2019
Better solvers for properness/contractiveness

#249 · created Jun 21, 2019 by Paolo G. Giarrusso
- CLOSED
- 4
updated Feb 13, 2020
Comparison with `=` and with CAS is not the same

#248 · created Jun 18, 2019 by Ralf Jung T-heap_lang
- CLOSED
- 1
- 25
updated Jul 01, 2019
iInv does not behave as intended when the goal is an accessor

#247 · created Jun 18, 2019 by Ralf Jung
- CLOSED
- 1
updated Nov 01, 2019
iEval (eauto) "corrupts" goal

#246 · created Jun 14, 2019 by Paolo G. Giarrusso
- CLOSED
- 1
updated Jun 15, 2019