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
Become part of Coq Platform?
#332
· opened
Jul 05, 2020
by
Ralf Jung
A-coq
A-meta
3
5
updated
Jul 21, 2020
simpl breaks error checking of `iNext (S i)`
#331
· opened
Jun 29, 2020
by
Paolo G. Giarrusso
A-coq
C-bug
T-proofmode
1
3
updated
Jul 14, 2020
Consider adding `iEnough` variants of `iAssert` ?
#330
· opened
Jun 25, 2020
by
Paolo G. Giarrusso
A-coq
C-enhancement
T-proofmode
3
updated
Jun 26, 2020
Iris Website Reform
#329
· opened
Jun 25, 2020
by
Ralf Jung
A-infra
A-meta
C-project
3
1
updated
Sep 29, 2020
Add RA for auth of a heap
#328
· opened
Jun 23, 2020
by
Ralf Jung
A-coq
C-enhancement
T-algebra
CLOSED
1
5
updated
Oct 12, 2020
Add RA for auth max_nat
#327
· opened
Jun 19, 2020
by
Robbert Krebbers
A-coq
C-enhancement
T-algebra
CLOSED
1
2
0
updated
Oct 27, 2020
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
Make `contractive_proper` into a lemma, or control other instances that make it costly.
#321
· opened
May 27, 2020
by
Paolo G. Giarrusso
A-coq
C-enhancement
I-performance
T-algebra
1
1
updated
Oct 20, 2020
λne should use %I for body — or add a variant using `%I`.
#320
· opened
May 27, 2020
by
Paolo G. Giarrusso
A-coq
C-enhancement
T-algebra
4
updated
Jul 14, 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
Use `byte` based strings for proof mode
#317
· opened
May 12, 2020
by
Robbert Krebbers
A-coq
C-enhancement
I-performance
T-proofmode
1
7
updated
May 16, 2020
Explore use of `#[local]`/`Local` definitions
#316
· opened
May 08, 2020
by
Ralf Jung
A-coq
C-enhancement
T-style
2
updated
Oct 02, 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
Fix setoid rewriting for function application in Iris
#312
· opened
Apr 22, 2020
by
Paolo G. Giarrusso
A-coq
C-enhancement
T-algebra
3
updated
Apr 22, 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
Prev
1
2
3
4
5
6
7
8
…
20
Next