Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Iris
Iris
Issues
Open
96
Closed
38
All
134
New issue
Recent searches
{{formattedKey}}
{{ title }}
{{ help }}
{{name}}
@{{username}}
None
Any
{{name}}
@{{username}}
None
Any
{{name}}
@{{username}}
None
Any
{{name}}
@{{username}}
None
Any
Upcoming
Started
{{title}}
None
Any
{{title}}
None
Any
{{title}}
None
Any
{{name}}
Yes
No
Yes
No
{{title}}
{{title}}
Created date
Priority
Created date
Last updated
Milestone due date
Due date
Popularity
Label priority
Manual
Make string-ident a standard part of Iris
#404
· opened
Feb 15, 2021
by
Lennard Gäher
A-coq
C-enhancement
T-proofmode
1
2
1
updated
Feb 17, 2021
Iris 3.4
#403
· opened
Feb 12, 2021
by
Ralf Jung
A-coq
C-tracking-issue
0
updated
Feb 17, 2021
iFrame performance issues
#402
· opened
Feb 03, 2021
by
Ralf Jung
A-coq
C-enhancement
I-performance
T-proofmode
0
updated
Feb 17, 2021
Upstream more big_op lemmas from Perennial
#399
· opened
Jan 27, 2021
by
Ralf Jung
A-coq
C-enhancement
T-bi
1
updated
Feb 17, 2021
Use `dom` instead of `∀ k, is_Some (.. !! k) ...`
#398
· opened
Jan 26, 2021
by
Robbert Krebbers
A-coq
C-enhancement
T-algebra
T-bi
0
updated
Feb 17, 2021
`iRename` fails with bad error message when not in proof mode
#397
· opened
Jan 12, 2021
by
Robbert Krebbers
A-coq
C-bug
Good First Issue
T-proofmode
1
updated
Feb 17, 2021
Intro pattern `>` has wrong behavior with side-conditions of `iMod`
#396
· opened
Jan 12, 2021
by
Robbert Krebbers
A-coq
C-bug
T-proofmode
3
updated
Feb 17, 2021
Generalize frac to dfrac in view camera
#395
· opened
Jan 04, 2021
by
Simon Friis Vindum
A-coq
C-enhancement
T-algebra
1
3
updated
Jan 25, 2021
Add append-only list RA to Iris
#391
· opened
Dec 08, 2020
by
Ralf Jung
A-coq
C-enhancement
T-algebra
T-base_logic
1
updated
Feb 05, 2021
reshape_expr does not recognize `fill`
#385
· opened
Nov 27, 2020
by
Ralf Jung
A-coq
C-enhancement
T-heap_lang
0
updated
Dec 05, 2020
Make sure we have Hint Mode for every typeclass
0 of 1 task completed
#381
· opened
Nov 12, 2020
by
Ralf Jung
A-coq
C-bug
T-style
0
updated
Nov 12, 2020
iDestruct does not handle some patterns that it probably could
#380
· opened
Nov 11, 2020
by
Tej Chajed
A-coq
C-enhancement
T-proofmode
1
0
updated
Nov 11, 2020
Make sealing consistent and document it
#379
· opened
Nov 10, 2020
by
Ralf Jung
A-coq
A-docs
C-enhancement
T-style
0
updated
Nov 10, 2020
Graveyard for obsolete code
#378
· opened
Nov 10, 2020
by
Robbert Krebbers
A-coq
4
updated
Feb 03, 2021
We have some lonely notations
#375
· opened
Nov 05, 2020
by
Ralf Jung
A-coq
C-bug
T-style
0
updated
Nov 05, 2020
Avoid sequences of "_" by adjusting lemma statements
#374
· opened
Nov 05, 2020
by
Ralf Jung
A-coq
C-enhancement
T-style
0
updated
Nov 05, 2020
Add validI lemmas for discrete RAs
0 of 4 tasks completed
#371
· opened
Nov 02, 2020
by
Ralf Jung
A-coq
C-enhancement
T-algebra
1
updated
Nov 05, 2020
Remove `inv` lemmas for agree/auth/view/etc and add `_L` variants to the ↔ lemma
#368
· opened
Oct 21, 2020
by
Robbert Krebbers
A-coq
C-enhancement
T-algebra
8
updated
Nov 04, 2020
`Export` everywhere does not permit consistent shadowing
#366
· opened
Oct 16, 2020
by
Ralf Jung
A-coq
C-project
8
updated
Nov 05, 2020
Implement typeclasses analogous to Fractional and AsFractional for discardable fractions
#364
· opened
Oct 15, 2020
by
Tej Chajed
A-coq
C-enhancement
T-base_logic
1
updated
Oct 21, 2020
Prev
1
2
3
4
5
Next