Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
I
Iris
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
122
Issues
122
List
Boards
Labels
Service Desk
Milestones
Merge Requests
18
Merge Requests
18
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Incidents
Environments
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Iris
Iris
Issues
Open
122
Closed
263
All
385
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
iSpecialize with "[% //]" does not report an error if done fails
#325
· opened
Jun 12, 2020
by
Tej Chajed
CLOSED
1
0
updated
Jun 26, 2020
Add "nat+min" RA
#324
· opened
Jun 12, 2020
by
Ralf Jung
C-enhancement
T-algebra
CLOSED
1
9
updated
Jun 18, 2020
Operator precedence in heap lang is wrong
#322
· opened
May 28, 2020
by
Dmitry Khalanskiy
CLOSED
4
updated
May 28, 2020
Fix "omega is deprecated" warnings by switching to lia
#319
· opened
May 16, 2020
by
Tej Chajed
CLOSED
1
2
updated
May 16, 2020
Drop support for Coq 8.9?
#318
· opened
May 12, 2020
by
Ralf Jung
A-coq
CLOSED
1
2
updated
Aug 24, 2020
Port HeapLang tactics to more efficient style
#315
· opened
Apr 29, 2020
by
Robbert Krebbers
A-coq
C-enhancement
I-performance
T-heap_lang
CLOSED
1
0
updated
Jul 15, 2020
Argument to bi_pure should have argument at type_scope?
#314
· opened
Apr 26, 2020
by
Gregory Malecha
A-coq
C-enhancement
CLOSED
5
updated
Apr 28, 2020
Add deallocation operation to HeapLang
#313
· opened
Apr 23, 2020
by
Ralf Jung
C-enhancement
T-heap_lang
CLOSED
1
0
updated
May 25, 2020
Document side-effects of importing Iris
#311
· opened
Apr 21, 2020
by
Ralf Jung
A-coq
A-docs
C-enhancement
CLOSED
1
3
updated
Sep 29, 2020
Fix name duplication `elem_of_list_singleton` in Iris and std++
#309
· opened
Apr 07, 2020
by
Robbert Krebbers
Iris 3.3
A-coq
C-bug
T-algebra
CLOSED
1
18
updated
Jul 15, 2020
`iIntros "%"` no longer works with universal quantification
#307
· opened
Apr 07, 2020
by
Ralf Jung
CLOSED
1
10
updated
Apr 07, 2020
Iris 3.3 release planning
8 of 8 tasks completed
#306
· opened
Apr 07, 2020
by
Ralf Jung
Iris 3.3
A-coq
C-project
CLOSED
1
updated
Jul 15, 2020
Update `proof_mode.md` for !400
#305
· opened
Apr 07, 2020
by
Robbert Krebbers
Iris 3.3
A-docs
C-bug
T-proofmode
CLOSED
1
0
updated
Apr 07, 2020
Notation `(⊢@{PROP})` and `(⊣⊢@{PROP} )` broken
#302
· opened
Mar 30, 2020
by
Robbert Krebbers
A-coq
C-bug
T-bi
CLOSED
2
12
updated
May 24, 2020
`iExists` ignores `Opaque`
#301
· opened
Mar 29, 2020
by
Paolo G. Giarrusso
A-coq
C-bug
S-blocked-by-coq
T-bi
CLOSED
10
updated
Mar 30, 2020
`leibnizO` finds convoluted proof for definitions
#299
· opened
Mar 12, 2020
by
Robbert Krebbers
A-coq
C-bug
T-algebra
CLOSED
1
3
updated
Mar 12, 2020
Use Coq deprecation attribute to implement deprecations
#296
· opened
Feb 29, 2020
by
Tej Chajed
Iris 3.3
A-coq
C-enhancement
CLOSED
1
1
0
updated
Jul 15, 2020
Add `array_copy` function in HeapLang
#293
· opened
Feb 20, 2020
by
Robbert Krebbers
T-heap_lang
CLOSED
1
3
updated
Feb 25, 2020
iExists fails if goal after the existential quantifier is an evar
#288
· opened
Feb 06, 2020
by
Michael Sammler
A-coq
C-bug
T-proofmode
CLOSED
1
0
updated
Dec 10, 2020
Remove eta-expansions from sealed definitions
#285
· opened
Jan 15, 2020
by
Ralf Jung
A-coq
C-enhancement
T-style
CLOSED
1
0
updated
Aug 30, 2020
Prev
1
2
3
4
5
6
…
14
Next