Issues · Iris · GitLab

Associativity of insert notation is awkard: `<[ k := v ]> m`

stdpp#59 · opened Apr 01, 2020 by Gregory Malecha
- 8
updated Apr 02, 2020
Notation `(⊢@{PROP})` and `(⊣⊢@{PROP} )` broken

iris#302 · opened Mar 30, 2020 by Robbert
- 1
- 12
updated Mar 31, 2020
stdpp breaks setoid rewriting

stdpp#58 · opened Mar 30, 2020 by sarahzrf
- 7
updated Apr 01, 2020
vs doesn't use FUpd

iris#300 · opened Mar 28, 2020 by Gregory Malecha A-coq C-enhancement T-base_logic T-bi
- 4
updated Mar 30, 2020
Add CI to this repository

tutorial-popl20#1 · opened Mar 18, 2020 by Ralf Jung
- 0
updated Mar 18, 2020
Updating the type system and program context typing 0 of 4 tasks completed

reloc#7 · opened Mar 06, 2020 by Dan Frumin
- 0
updated Mar 06, 2020
Guide typeclass search via more specialized typeclasses

iris#298 · opened Mar 06, 2020 by Michael Sammler A-coq C-enhancement I-performance
- 1
updated Mar 06, 2020
Persistent (and other BI class) instances missing for telescopes

iris#297 · opened Mar 05, 2020 by Robbert A-coq C-enhancement T-bi
- 0
updated Mar 05, 2020
Use Coq deprecation attribute to implement deprecations

iris#296 · opened Feb 29, 2020 by Tej Chajed Iris 3.3 A-coq C-enhancement
- 1
- 0
updated Mar 18, 2020
Have iApply introduce equalities for subterms that cannot be unified directly

iris#295 · opened Feb 24, 2020 by Armaël Guéneau A-coq C-enhancement T-proofmode
- 1
- 3
updated Mar 06, 2020
stdpp.base.decide := Coq.Classes.DecidableClass.decide?

stdpp#51 · opened Feb 11, 2020 by Abhishek Anand
- 5
updated Feb 17, 2020
Possible redesign of handling of persistent/intuitionistic propositions in intro patterns

iris#290 · opened Feb 11, 2020 by Ralf Jung A-coq C-enhancement T-proofmode
- 1
updated Feb 11, 2020
Make coPset operations TC opaque

stdpp#48 · opened Feb 10, 2020 by Robbert
- 3
updated Feb 18, 2020
Documentation for installation on Windows

iris#289 · opened Feb 06, 2020 by Ralf Jung A-docs C-enhancement
- 0
updated Feb 06, 2020
iApply strips some modalities, but not monotonically

iris#287 · opened Jan 31, 2020 by Paolo G. Giarrusso A-coq C-bug T-proofmode
- 1
updated Feb 01, 2020
Address the STS encodings lack of usefulness

iris#286 · opened Jan 30, 2020 by Jonas Kastberg A-coq C-enhancement T-algebra
- 1
- 5
updated Jan 30, 2020
Remove eta-expansions from sealed definitions

iris#285 · opened Jan 15, 2020 by Ralf Jung A-coq C-enhancement T-style
- 0
updated Jan 15, 2020
Documentation for installation on OS X

iris#280 · opened Dec 16, 2019 by Jules Jacobs A-docs C-enhancement
- 1
- 8
updated Feb 06, 2020
Write `wp_` lemmas for array operations in a more `iApply`/`wp_apply` friendly way

iris#278 · opened Dec 09, 2019 by Ralf Jung A-coq C-bug T-heap_lang
- 4
updated Dec 12, 2019
solve_ndisj taking a long time

stdpp#47 · opened Dec 03, 2019 by Jonas Kastberg
- 1
updated Dec 04, 2019

Prev
1
2
3
4
5
6
Next