Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Iris
Iris
Issues
Open
123
Closed
269
All
392
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
Use dfrac everywhere
0 of 7 tasks completed
#412
· created
Apr 19, 2021
by
Ralf Jung
A-coq
C-enhancement
T-algebra
T-base_logic
0
updated
Apr 19, 2021
Taking ∃ out of ▷ without Inhabited, more easily
#411
· created
Mar 28, 2021
by
Yusuke Matsushita
A-coq
C-enhancement
T-proofmode
3
updated
Mar 29, 2021
Modality for `Timeless`
#410
· created
Mar 22, 2021
by
Ralf Jung
A-theory
C-project
T-bi
1
2
updated
Apr 19, 2021
Proposed change to naming convention for "dataful" `*G`s
#409
· created
Mar 18, 2021
by
Ralf Jung
A-coq
C-enhancement
T-style
3
updated
Apr 19, 2021
bi.weakestpre imports a module from program_logic
#408
· created
Mar 17, 2021
by
Ralf Jung
A-coq
C-bug
T-bi
T-program_logic
2
7
updated
Mar 18, 2021
Tracking issue for list RA
#407
· created
Mar 17, 2021
by
Ralf Jung
C-tracking-issue
T-algebra
0
updated
Mar 17, 2021
Slow typechecking / nonterminating Qed when using auxiliary definitions in RAs
#406
· created
Mar 03, 2021
by
Armaël Guéneau
A-coq
C-bug
I-performance
T-algebra
3
updated
Mar 18, 2021
Tracking issue for HeapLang interpreter
#405
· created
Feb 16, 2021
by
Ralf Jung
C-tracking-issue
T-heap_lang
0
updated
Feb 16, 2021
iFrame performance issues
#402
· created
Feb 03, 2021
by
Ralf Jung
A-coq
C-enhancement
I-performance
T-proofmode
1
0
updated
Feb 17, 2021
Integrate Tej's simp-lang?
#400
· created
Jan 28, 2021
by
Ralf Jung
A-docs
T-program_logic
5
updated
Feb 17, 2021
Upstream more big_op lemmas from Perennial
#399
· created
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
· created
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
· created
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
· created
Jan 12, 2021
by
Robbert Krebbers
A-coq
C-bug
T-proofmode
3
updated
Feb 17, 2021
Document relation between Discrete and Timeless (in appendix?)
#394
· created
Dec 23, 2020
by
Paolo G. Giarrusso
A-docs
T-algebra
T-base_logic
0
updated
Jan 06, 2021
Masks in step-taking fupd notation
#392
· created
Dec 10, 2020
by
Ralf Jung
A-theory
C-enhancement
T-base_logic
1
0
updated
Dec 10, 2020
Add append-only list RA to Iris
#391
· created
Dec 08, 2020
by
Ralf Jung
A-coq
C-enhancement
T-algebra
T-base_logic
1
1
updated
Apr 05, 2021
Citation guide
#389
· created
Dec 06, 2020
by
Tej Chajed
A-docs
1
updated
Dec 08, 2020
reshape_expr does not recognize `fill`
#385
· created
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
· created
Nov 12, 2020
by
Ralf Jung
A-coq
C-bug
T-style
0
updated
Nov 12, 2020
Prev
1
2
3
4
5
…
7
Next