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
120
Closed
266
All
386
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}}
Label priority
Priority
Created date
Last updated
Milestone due date
Due date
Popularity
Label priority
Manual
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
Reliance on `Export` bug
#254
· opened
Jul 09, 2019
by
Maxime Dénès
CLOSED
5
updated
Nov 01, 2019
Constructing CMRAs by giving isomorphism to CMRAs
#253
· opened
Jul 09, 2019
by
Paolo G. Giarrusso
A-coq
C-enhancement
Good First Issue
T-algebra
CLOSED
1
1
5
updated
Nov 06, 2020
equivI lemma for sigT
#250
· opened
Jun 24, 2019
by
Paolo G. Giarrusso
CLOSED
1
4
updated
Jun 25, 2019
Better solvers for properness/contractiveness
#249
· opened
Jun 21, 2019
by
Paolo G. Giarrusso
CLOSED
4
updated
Feb 13, 2020
Comparison with `=` and with CAS is not the same
#248
· opened
Jun 18, 2019
by
Ralf Jung
T-heap_lang
CLOSED
1
25
updated
Jul 01, 2019
iInv does not behave as intended when the goal is an accessor
#247
· opened
Jun 18, 2019
by
Ralf Jung
CLOSED
1
updated
Nov 01, 2019
iEval (eauto) "corrupts" goal
#246
· opened
Jun 14, 2019
by
Paolo G. Giarrusso
CLOSED
1
updated
Jun 15, 2019
Add IntoAnd instance (and more) for array
#245
· opened
Jun 14, 2019
by
Rodolphe Lepigre
Iris 3.2
CLOSED
1
updated
Aug 13, 2019
Planning the Iris 3.2 release
0 of 1 task completed
#242
· opened
Jun 06, 2019
by
Ralf Jung
Iris 3.2
A-meta
C-enhancement
CLOSED
1
1
3
updated
Nov 01, 2019
We have ambiguous coercion paths
#240
· opened
May 13, 2019
by
Ralf Jung
A-coq
C-bug
T-algebra
CLOSED
1
7
updated
Apr 02, 2020
Iris logo
#239
· opened
May 06, 2019
by
Robbert Krebbers
A-meta
C-project
CLOSED
27
updated
Feb 05, 2021
Wish: iSimpl on multiple hypothesis
#238
· opened
Apr 26, 2019
by
Dan Frumin
C-enhancement
T-proofmode
CLOSED
1
0
updated
May 22, 2019
Stripping laterN from pure propositions when proving laterN *without except-0*
#237
· opened
Apr 15, 2019
by
Paolo G. Giarrusso
CLOSED
2
updated
Nov 01, 2019
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
Syntactic type system for heap_lang
0 of 2 tasks completed
#234
· opened
Mar 29, 2019
by
Robbert Krebbers
A-theory
C-project
T-heap_lang
CLOSED
31
updated
Oct 01, 2020
Can't install on Coq 8.8.1
#233
· opened
Mar 19, 2019
by
Maximilian Wuttke
CLOSED
2
updated
Mar 20, 2019
Investigate slowdown caused by gset change
#232
· opened
Mar 14, 2019
by
Ralf Jung
CLOSED
1
9
updated
Apr 24, 2019
Allow swapping later^i and forall, later, etc.
#231
· opened
Mar 02, 2019
by
Paolo G. Giarrusso
CLOSED
4
updated
Nov 01, 2019
"Generalizable All Variables" considered harmful
#230
· opened
Feb 22, 2019
by
Ralf Jung
CLOSED
4
updated
Feb 27, 2019
Prev
1
2
3
4
5
6
7
8
…
14
Next