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
116
Issues
116
List
Boards
Labels
Service Desk
Milestones
Merge Requests
23
Merge Requests
23
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
27
Closed
6
All
33
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
`Export` everywhere does not permit consistent shadowing
#366
· opened
Oct 16, 2020
by
Ralf Jung
A-coq
C-project
8
updated
Nov 05, 2020
Tracking issue for records
#352
· opened
Sep 29, 2020
by
Ralf Jung
Iris 3.4
A-coq
C-project
T-records
4
updated
Dec 05, 2020
Iris Website Reform
#329
· opened
Jun 25, 2020
by
Ralf Jung
A-infra
A-meta
C-project
3
1
updated
Sep 29, 2020
Investigate use of "Filtered Unification"
#264
· opened
Aug 31, 2019
by
Ralf Jung
A-coq
C-project
0
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
"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
Iris logo
#239
· opened
May 06, 2019
by
Robbert
A-meta
C-project
26
updated
Aug 22, 2020
"expression validity" in WP
#228
· opened
Feb 19, 2019
by
Jonas Kastberg
A-theory
C-project
T-program_logic
19
updated
Nov 01, 2019
Provide a convenient way to define non-recursive ghost state
#227
· opened
Feb 19, 2019
by
Ralf Jung
A-coq
A-theory
C-project
T-algebra
T-base_logic
1
5
updated
Dec 07, 2020
Define persistence otherwise (and get rid of core)
#224
· opened
Dec 18, 2018
by
Ralf Jung
A-theory
C-project
T-bi
1
21
updated
Aug 28, 2020
iMod: Control which modality is reduced
#212
· opened
Oct 03, 2018
by
Ralf Jung
A-coq
C-project
T-proofmode
10
updated
Nov 01, 2019
Generic subset construction for RAs
#210
· opened
Aug 29, 2018
by
Ralf Jung
A-theory
C-project
T-algebra
2
updated
Sep 08, 2020
Make notation for pure and plainly affine
#205
· opened
Jul 13, 2018
by
Ralf Jung
A-coq
C-project
T-linear
1
updated
Sep 29, 2020
Stronger/Weaker iFrame
#183
· opened
Apr 20, 2018
by
Ralf Jung
A-coq
C-project
T-proofmode
5
updated
Nov 01, 2019
Explore performance implications of gen_proofmode
#180
· opened
Apr 10, 2018
by
Ralf Jung
A-coq
C-project
I-performance
T-proofmode
3
updated
Nov 01, 2019
String-free proofterms
#172
· opened
Mar 10, 2018
by
Ralf Jung
A-coq
C-project
I-performance
T-proofmode
6
updated
Sep 08, 2020
iSpecialize on implications behaves inconsistently
#168
· opened
Mar 07, 2018
by
Ralf Jung
A-coq
C-project
T-proofmode
7
updated
Nov 01, 2019
iDestruct on a conjunction magically transforms hypothesis
#166
· opened
Mar 07, 2018
by
Ralf Jung
A-coq
C-project
T-linear
T-proofmode
15
updated
Nov 01, 2019
Better (?) approach to control typeclass resolution based on whether some arguments are evars
#165
· opened
Mar 06, 2018
by
Ralf Jung
A-coq
C-project
T-proofmode
0
updated
Nov 01, 2019
Prev
1
2
Next