Issues · Iris / Iris · GitLab

`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
Non-expansiveness for big ops

#236 · opened Apr 07, 2019 by Dan Frumin A-coq C-enhancement Good First Issue T-bi
- CLOSED
- 4
updated Mar 19, 2020
Failure to find a proof of persistence

#255 · opened Jul 19, 2019 by Dmitry Khalanskiy A-coq C-bug S-blocked-by-coq T-algebra
- CLOSED
- 1
- 12
updated Mar 18, 2020
Masks are coPsets in the Coq development, not arbitrary subsets of natural numbers

#211 · opened Oct 01, 2018 by Joseph Tassarotti A-docs C-enhancement
- CLOSED
- 1
- 1
updated Mar 18, 2020
Use `plainly_alt` as an axiom and replace most of the current ones

#161 · opened Feb 26, 2018 by Jacques-Henri Jourdan A-theory C-project T-bi
- CLOSED
- 66
updated Mar 18, 2020
Stronger `list_core_id`

#258 · opened Aug 06, 2019 by Dmitry Khalanskiy A-coq C-enhancement Good First Issue T-algebra
- CLOSED
- 6
updated Mar 18, 2020
`leibnizO` finds convoluted proof for definitions

#299 · opened Mar 12, 2020 by Robbert A-coq C-bug T-algebra
- CLOSED
- 1
- 3
updated Mar 12, 2020
Odd Behavior for Substitution

#229 · opened Feb 20, 2019 by Daniel Gratzer
- CLOSED
- 6
updated Mar 12, 2020
Add `array_copy` function in HeapLang

#293 · opened Feb 20, 2020 by Robbert T-heap_lang
- CLOSED
- 1
- 3
updated Feb 25, 2020
Moving hypotheses from the intuitionistic to the spatial context

#213 · opened Oct 04, 2018 by Robbert A-coq C-enhancement T-proofmode
- CLOSED
- 1
- 0
updated Feb 18, 2020
Better solvers for properness/contractiveness

#249 · opened Jun 21, 2019 by Paolo G. Giarrusso
- CLOSED
- 4
updated Feb 13, 2020
Editor bindings for Emacs and m17n are inconsistent

#279 · opened Dec 14, 2019 by Tej Chajed A-docs C-enhancement
- CLOSED
- 5
updated Feb 11, 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 Feb 10, 2020
Editor config should explain how to configure CoqIDE 8.10 unicode input

#269 · opened Oct 19, 2019 by Tej Chajed A-docs C-enhancement
- CLOSED
- 1
- 1
updated Feb 10, 2020
Formalize example that impredicative invariants and linearity are incompatible

#132 · opened Jan 09, 2018 by Robbert A-coq C-enhancement T-linear
- CLOSED
- 1
- 4
updated Feb 07, 2020
Undesired simplification behaviour of big_sepM2

#282 · opened Dec 20, 2019 by Michael Sammler A-coq C-bug T-bi
- CLOSED
- 6
updated Feb 05, 2020
fupd_proper is too weak

#284 · opened Jan 04, 2020 by Abhishek Anand C-support
- CLOSED
- 1
- 7
updated Jan 06, 2020
big_sepM2_fmap and friends only work for nat keys

#283 · opened Dec 20, 2019 by Michael Sammler
- CLOSED
- 1
- 1
- 2
updated Dec 20, 2019
proof_mode.md documentation has a broken link

#281 · opened Dec 19, 2019 by Jules Jacobs A-docs C-bug
- CLOSED
- 1
- 2
updated Dec 19, 2019
`iIntoValid` failing in an unexpected way

#140 · opened Jan 18, 2018 by Jacques-Henri Jourdan A-coq C-bug T-proofmode
- CLOSED
- 9
updated Dec 03, 2019

Prev
1
2
3
4
5
6
…
12
Next