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}}
Milestone due date
Priority
Created date
Last updated
Milestone due date
Due date
Popularity
Label priority
Manual
Proof mode only *mostly* works when it is transitively imported, not exported
#111
· opened
Nov 16, 2017
by
Ralf Jung
Iris 3.1
T-proofmode
CLOSED
7
updated
Nov 20, 2017
iIntros on pure implications stopped working
#108
· opened
Oct 28, 2017
by
Ralf Jung
Iris 3.1
T-proofmode
CLOSED
7
updated
Oct 28, 2017
Reverting to old (stronger) definition of atomicity
#107
· opened
Oct 27, 2017
by
Amin Timany
Iris 3.1
CLOSED
1
17
updated
Oct 29, 2017
Iris 3.1
3 of 4 tasks completed
#106
· opened
Oct 27, 2017
by
Ralf Jung
Iris 3.1
CLOSED
8
updated
Jan 09, 2018
Add some theory about the interaction of plainly and fancy updates
#105
· opened
Oct 27, 2017
by
Ralf Jung
Iris 3.1
CLOSED
1
2
updated
Nov 01, 2017
Proof mode notation broken depending on import order
#100
· opened
Sep 29, 2017
by
Ralf Jung
Iris 3.1
T-proofmode
CLOSED
15
updated
Nov 11, 2017
Let iAlways clear the spatial context
#81
· opened
Mar 16, 2017
by
Ralf Jung
Iris 3.1
T-proofmode
CLOSED
16
updated
Oct 27, 2017
Stronger Invariant Allocation Rules
#59
· opened
Dec 29, 2016
by
Janno
Iris 3.0
CLOSED
9
updated
Jan 11, 2017
iAssert ... as %X should get all assumptions
#56
· opened
Dec 20, 2016
by
Ralf Jung
Iris 3.0
T-proofmode
CLOSED
1
updated
Jan 03, 2017
iNext unfolds things (more than simpl) even when there is no later to strip
#55
· opened
Dec 20, 2016
by
Ralf Jung
Iris 3.0
T-proofmode
CLOSED
10
updated
Feb 20, 2018
iIntros fails to introduce Coq-level and Iris-level universal quantifiers at once
#54
· opened
Dec 19, 2016
by
Ralf Jung
Iris 3.0
T-proofmode
CLOSED
3
updated
Dec 21, 2016
iMod and evar instantiation
#52
· opened
Dec 19, 2016
by
Ralf Jung
Iris 3.0
T-proofmode
CLOSED
4
updated
Jun 17, 2019
`contains` is named the wrong way around
#50
· opened
Dec 14, 2016
by
Ralf Jung
Iris 3.0
CLOSED
42
updated
Jan 14, 2017
Use opam-based CI
#47
· opened
Nov 30, 2016
by
Ralf Jung
Iris 3.0
CLOSED
2
updated
Dec 14, 2016
Renaming things
#35
· opened
Sep 29, 2016
by
Ralf Jung
Iris 3.0
CLOSED
42
updated
Nov 09, 2016
wp_bind does not report a failure message
#401
· opened
Feb 02, 2021
by
Tej Chajed
CLOSED
1
0
updated
Feb 02, 2021
fupd_plainly_laterN = fupd_plain_laterN ?
#393
· opened
Dec 23, 2020
by
Paolo G. Giarrusso
CLOSED
1
1
updated
Dec 23, 2020
Dropping support for Coq 8.10
#388
· opened
Dec 04, 2020
by
Tej Chajed
A-coq
CLOSED
1
1
2
updated
Dec 16, 2020
Deprecate unqualified "Instance"
#387
· opened
Dec 03, 2020
by
Ralf Jung
A-coq
C-enhancement
T-style
CLOSED
4
updated
Dec 19, 2020
Quote does not handle ⊣⊢
#373
· opened
Nov 03, 2020
by
Rodolphe Lepigre
CLOSED
1
updated
Nov 05, 2020
Prev
1
2
3
4
5
6
…
14
Next