Issues · Iris / Iris · GitLab

iSpecialize with "[% //]" does not report an error if done fails

#325 · opened Jun 12, 2020 by Tej Chajed
- CLOSED
- 1
- 0
updated Jun 26, 2020
Add "nat+min" RA

#324 · opened Jun 12, 2020 by Ralf Jung C-enhancement T-algebra
- CLOSED
- 1
- 9
updated Jun 18, 2020
Operator precedence in heap lang is wrong

#322 · opened May 28, 2020 by Dmitry Khalanskiy
- CLOSED
- 4
updated May 28, 2020
Fix "omega is deprecated" warnings by switching to lia

#319 · opened May 16, 2020 by Tej Chajed
- CLOSED
- 1
- 2
updated May 16, 2020
Drop support for Coq 8.9?

#318 · opened May 12, 2020 by Ralf Jung A-coq
- CLOSED
- 1
- 2
updated Aug 24, 2020
Port HeapLang tactics to more efficient style

#315 · opened Apr 29, 2020 by Robbert Krebbers A-coq C-enhancement I-performance T-heap_lang
- CLOSED
- 1
- 0
updated Jul 15, 2020
Argument to bi_pure should have argument at type_scope?

#314 · opened Apr 26, 2020 by Gregory Malecha A-coq C-enhancement
- CLOSED
- 5
updated Apr 28, 2020
Add deallocation operation to HeapLang

#313 · opened Apr 23, 2020 by Ralf Jung C-enhancement T-heap_lang
- CLOSED
- 1
- 0
updated May 25, 2020
Document side-effects of importing Iris

#311 · opened Apr 21, 2020 by Ralf Jung A-coq A-docs C-enhancement
- CLOSED
- 1
- 3
updated Sep 29, 2020
Fix name duplication `elem_of_list_singleton` in Iris and std++

#309 · opened Apr 07, 2020 by Robbert Krebbers Iris 3.3 A-coq C-bug T-algebra
- CLOSED
- 1
- 18
updated Jul 15, 2020
`iIntros "%"` no longer works with universal quantification

#307 · opened Apr 07, 2020 by Ralf Jung
- CLOSED
- 1
- 10
updated Apr 07, 2020
Iris 3.3 release planning 8 of 8 tasks completed

#306 · opened Apr 07, 2020 by Ralf Jung Iris 3.3 A-coq C-project
- CLOSED
- 1
updated Jul 15, 2020
Update `proof_mode.md` for !400

#305 · opened Apr 07, 2020 by Robbert Krebbers Iris 3.3 A-docs C-bug T-proofmode
- CLOSED
- 1
- 0
updated Apr 07, 2020
Notation `(⊢@{PROP})` and `(⊣⊢@{PROP} )` broken

#302 · opened Mar 30, 2020 by Robbert Krebbers A-coq C-bug T-bi
- CLOSED
- 2
- 12
updated May 24, 2020
`iExists` ignores `Opaque`

#301 · opened Mar 29, 2020 by Paolo G. Giarrusso A-coq C-bug S-blocked-by-coq T-bi
- CLOSED
- 10
updated Mar 30, 2020
`leibnizO` finds convoluted proof for definitions

#299 · opened Mar 12, 2020 by Robbert Krebbers A-coq C-bug T-algebra
- CLOSED
- 1
- 3
updated Mar 12, 2020
Use Coq deprecation attribute to implement deprecations

#296 · opened Feb 29, 2020 by Tej Chajed Iris 3.3 A-coq C-enhancement
- CLOSED
- 1
- 1
- 0
updated Jul 15, 2020
Add `array_copy` function in HeapLang

#293 · opened Feb 20, 2020 by Robbert Krebbers T-heap_lang
- CLOSED
- 1
- 3
updated Feb 25, 2020
iExists fails if goal after the existential quantifier is an evar

#288 · opened Feb 06, 2020 by Michael Sammler A-coq C-bug T-proofmode
- CLOSED
- 1
- 0
updated Dec 10, 2020
Remove eta-expansions from sealed definitions

#285 · opened Jan 15, 2020 by Ralf Jung A-coq C-enhancement T-style
- CLOSED
- 1
- 0
updated Aug 30, 2020

Prev
1
2
3
4
5
6
…
14
Next