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
iMod should be able to eliminate <pers> and <plain> in the intuitionistic context
#167
· opened
Mar 07, 2018
by
Ralf Jung
A-coq
C-enhancement
T-proofmode
8
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
Dealing with nested modalities in `iModIntro`
1 of 3 tasks completed
#163
· opened
Feb 28, 2018
by
Robbert Krebbers
A-coq
C-project
T-proofmode
33
updated
Jun 29, 2020
iRewrite: Support rewriting with Coq hypotheses
#152
· opened
Feb 07, 2018
by
Ralf Jung
A-coq
C-enhancement
T-proofmode
0
updated
Nov 01, 2019
Smarter iFrame: Prefer framing below `*` over framing below disjunction or wand
#150
· opened
Feb 06, 2018
by
Ralf Jung
A-coq
C-project
T-proofmode
0
updated
Nov 01, 2019
Better names and documentation for proof mode typeclasses
#139
· opened
Jan 18, 2018
by
Ralf Jung
A-docs
C-enhancement
T-proofmode
8
updated
Nov 23, 2020
wp_apply/Texan triple improvements
0 of 4 tasks completed
#138
· opened
Jan 18, 2018
by
Ralf Jung
A-theory
C-enhancement
T-program_logic
T-proofmode
2
updated
Nov 26, 2020
Iris-internal solve_proper
#137
· opened
Jan 18, 2018
by
Ralf Jung
A-coq
C-project
T-proofmode
0
updated
Nov 01, 2019
Use [notypeclasses refine] for all proofmode tactics
#135
· opened
Jan 16, 2018
by
Robbert Krebbers
A-coq
C-enhancement
T-proofmode
9
updated
Nov 11, 2020
Document language interface
#134
· opened
Jan 13, 2018
by
Robbert Krebbers
A-docs
C-enhancement
T-program_logic
3
updated
Nov 01, 2019
Make iApply "with" specialization lazier
#130
· opened
Jan 08, 2018
by
Robbert Krebbers
A-coq
C-project
T-proofmode
1
updated
Nov 01, 2019
Make `iClear` work when there is at least one absorbing spatial hypothesis
#125
· opened
Dec 08, 2017
by
Robbert Krebbers
A-coq
C-enhancement
T-proofmode
0
updated
Nov 01, 2019
heap_lang: mutable n-ary locations, n-ary products, n-ary sums
#124
· opened
Dec 07, 2017
by
Ralf Jung
A-theory
C-project
T-heap_lang
5
updated
Nov 01, 2019
Add a general constructor from an affine BI
#123
· opened
Dec 06, 2017
by
Ralf Jung
A-coq
C-enhancement
T-bi
2
updated
Nov 01, 2019
Make some of the `wp_` tactics language independent
#117
· opened
Nov 30, 2017
by
Robbert Krebbers
A-coq
C-project
T-program_logic
T-proofmode
0
updated
Nov 01, 2019
smarter iIntros for plainly modality
0 of 1 task completed
#104
· opened
Oct 26, 2017
by
Robbert Krebbers
A-coq
C-enhancement
T-proofmode
2
updated
Nov 01, 2019
Support negative selection patterns
#89
· opened
May 12, 2017
by
Ralf Jung
A-coq
C-enhancement
T-proofmode
1
8
updated
Nov 01, 2019
Trouble with iApply and typeclass inference order
#78
· opened
Mar 15, 2017
by
Ralf Jung
A-coq
C-bug
T-proofmode
2
updated
Nov 01, 2019
iMod doesn't handle mismatched mask
#31
· opened
Aug 23, 2016
by
Ghost User
A-coq
C-enhancement
T-proofmode
1
20
updated
Oct 02, 2020
Prev
1
2
3
4
5
6
7
Next