Issues · Iris / Iris · GitLab

"Generalizable All Variables" considered harmful

#230 · opened Feb 22, 2019 by Ralf Jung
- 3
updated Feb 23, 2019
Introduction of predicate over expression in WP

#228 · opened Feb 19, 2019 by Jonas Kastberg
- 1
updated Feb 20, 2019
Provide a convenient way to define non-recursive ghost state

#227 · opened Feb 19, 2019 by Ralf Jung
- 1
- 2
updated Feb 20, 2019
Get rid of the core, define persistence otherwise

#224 · opened Dec 18, 2018 by Ralf Jung
- 8
updated Dec 21, 2018
Coqdocs should link to std++ coqdocs

#221 · opened Nov 30, 2018 by Ralf Jung
- 1
updated Nov 30, 2018
Replace most occurences of `.. || ..` by `first [..|..]`

#216 · opened Oct 14, 2018 by Robbert
- 2
updated Oct 15, 2018
Explore getting rid of implication

#215 · opened Oct 13, 2018 by Ralf Jung
- 7
updated Oct 15, 2018
Moving stuff out of the intuitionistic context

#213 · opened Oct 04, 2018 by Robbert Proofmode
- 0
updated Oct 04, 2018
iMod: Control which modality is reduced

#212 · opened Oct 03, 2018 by Ralf Jung Proofmode
- 10
updated Oct 05, 2018
Masks are coPsets in the Coq development, not arbitrary subsets of natural numbers

#211 · opened Oct 01, 2018 by Joseph Tassarotti
- 1
updated Oct 01, 2018
Generic subset construction for RAs

#210 · opened Aug 29, 2018 by Ralf Jung
- 2
updated Sep 18, 2018
Rule "Res-Alloc" in documentation is stronger than the Coq version

#207 · opened Aug 16, 2018 by Joseph Tassarotti
- 1
- 6
updated Feb 18, 2019
Make notation for pure and plainly affine

#205 · opened Jul 13, 2018 by Ralf Jung
- 1
updated Jul 31, 2018
Seal off local and frame-preserving update

#203 · opened Jul 05, 2018 by Ralf Jung
- 0
updated Jul 05, 2018
Use of `Into`/`From`/`As`/`Is` prefixes of classes is inconsistent

#202 · opened Jun 18, 2018 by Robbert
- 0
updated Jun 18, 2018
Extend `iApply` to deal with pure goals

#196 · opened Jun 07, 2018 by Glen Mével
- 1
- 0
updated Jun 07, 2018
Always qualify Instance with Local or Global

#195 · opened Jun 05, 2018 by Ralf Jung
- 0
updated Jun 05, 2018
eauto very slow when there is a chain of Iris quantifiers

#188 · opened May 23, 2018 by Ralf Jung Proofmode
- 1
updated May 24, 2018
iAssert without any spatial assumptions should produce a persistent results

#186 · opened Apr 24, 2018 by Ralf Jung Proofmode
- 0
updated Feb 17, 2019
"iApply ... with" unifies with assumptions before taking goal into account

#185 · opened Apr 23, 2018 by Ralf Jung Proofmode
- 1
updated Jul 13, 2018

Prev
1
2
3
4
Next