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
Documentation for installation on Windows
#289
· opened
Feb 06, 2020
by
Ralf Jung
A-docs
C-enhancement
0
updated
Feb 06, 2020
iApply strips some modalities, but not monotonically
#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
#286
· opened
Jan 30, 2020
by
Jonas Kastberg
A-coq
C-enhancement
T-algebra
1
5
updated
Jan 30, 2020
Documentation for installation on OS X
#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
#278
· opened
Dec 09, 2019
by
Ralf Jung
A-coq
C-bug
T-heap_lang
4
updated
Dec 12, 2019
Find a way to reduce usage of O/R/U suffixes
#277
· opened
Dec 02, 2019
by
Ralf Jung
A-coq
C-enhancement
T-algebra
0
updated
Dec 02, 2019
Create example user library and document library best practices
#276
· opened
Dec 02, 2019
by
Robbert Krebbers
A-docs
C-enhancement
T-style
1
2
updated
Sep 29, 2020
use implicit arguments for lemmas in coq_tactics.v
0 of 1 task completed
#275
· opened
Nov 22, 2019
by
Paolo G. Giarrusso
A-coq
C-enhancement
T-proofmode
0
updated
Nov 22, 2019
Iris shadows ssreflect new syntax
#273
· opened
Nov 07, 2019
by
Paolo G. Giarrusso
A-coq
C-bug
T-algebra
15
updated
Nov 22, 2019
Fix performance regressions in Iris and std++ in Coq 8.10.1 compared to Coq 8.9.0
#272
· opened
Nov 07, 2019
by
Robbert Krebbers
A-coq
I-performance
14
updated
Feb 12, 2020
`iInv`: support tokens that are "framed" around the accessor
#268
· opened
Sep 30, 2019
by
Dan Frumin
A-coq
C-enhancement
T-proofmode
1
updated
Mar 18, 2020
Inconsistent order of arguments for `inv_alloc` and `cinv_alloc`.
#267
· opened
Sep 30, 2019
by
Dan Frumin
A-coq
C-bug
T-base_logic
T-style
2
updated
Nov 01, 2019
Investigate use of "Filtered Unification"
#264
· opened
Aug 31, 2019
by
Ralf Jung
A-coq
C-project
0
updated
Nov 01, 2019
`big_op*_forall` that relate traversals over different structures
#262
· opened
Aug 28, 2019
by
Dmitry Khalanskiy
A-coq
C-enhancement
Good First Issue
T-algebra
6
updated
Jan 21, 2020
Provide smart `bi` constructor for BIs that are not step-indexed
#261
· opened
Aug 21, 2019
by
Robbert Krebbers
A-coq
C-enhancement
T-bi
1
0
updated
Nov 01, 2019
"Exponentiation" for separating conjunctions
#252
· opened
Jul 09, 2019
by
Dmitry Khalanskiy
A-coq
C-enhancement
Good First Issue
T-bi
3
updated
Nov 01, 2019
Simplification machinery for RA operations
#251
· opened
Jun 24, 2019
by
Ralf Jung
A-coq
C-project
T-algebra
1
1
updated
Apr 06, 2020
Add a general lattice RA to Iris
#244
· opened
Jun 12, 2019
by
Ralf Jung
A-theory
C-project
T-algebra
1
9
updated
Dec 10, 2020
Avoid type-level aliases for overloading of canonical structures
#243
· opened
Jun 11, 2019
by
Robbert Krebbers
A-coq
C-enhancement
T-algebra
0
updated
Nov 01, 2019
"Flattened" introduction patterns for intuitionistic conjunction elimination.
#241
· opened
May 27, 2019
by
Dan Frumin
A-coq
C-project
T-proofmode
2
updated
Nov 01, 2019
Prev
1
2
3
4
5
6
7
Next