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
iDestruct and iPureIntro
#21
· opened
Jul 27, 2016
by
Ghost User
A-coq
C-enhancement
T-proofmode
CLOSED
3
updated
Nov 01, 2019
Ticket lock proof
#22
· opened
Aug 01, 2016
by
Ghost User
CLOSED
0
updated
Aug 02, 2016
iFrame should support conjunction
#23
· opened
Aug 02, 2016
by
Ghost User
CLOSED
8
updated
Aug 02, 2016
Find nice syntax for our "CPS" WP specifications
#24
· opened
Aug 05, 2016
by
Ralf Jung
CLOSED
2
updated
Oct 27, 2016
iSplitL "persistent_hyp": Improve error
#25
· opened
Aug 05, 2016
by
Ralf Jung
T-proofmode
CLOSED
0
updated
Aug 06, 2016
heap-lang CAS capability
#26
· opened
Aug 08, 2016
by
Ghost User
CLOSED
14
updated
Oct 21, 2016
mathpartir.sty is missing
#27
· opened
Aug 09, 2016
by
Jeehoon Kang
CLOSED
3
updated
Aug 09, 2016
docs: the universe $\cal U$ is used without definition
#28
· opened
Aug 14, 2016
by
Jeehoon Kang
CLOSED
0
updated
Aug 16, 2016
Bring back Logically Atomic Triples (Coq + docs)
1 of 2 tasks completed
#29
· opened
Aug 16, 2016
by
Jeehoon Kang
A-theory
C-project
T-logical-atomicity
7
updated
Nov 01, 2019
Make coqchk (make verify) work
#30
· opened
Aug 19, 2016
by
Ralf Jung
CLOSED
5
updated
Aug 19, 2016
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
Support framing pure/Coq hypotheses
#32
· opened
Sep 05, 2016
by
Jacques-Henri Jourdan
CLOSED
5
updated
Sep 19, 2016
Confusing error msg for `iTimeless`
#33
· opened
Sep 12, 2016
by
Ghost User
T-proofmode
CLOSED
10
updated
Oct 27, 2016
Coq induction support in proof mode
#34
· opened
Sep 12, 2016
by
Jacques-Henri Jourdan
CLOSED
7
updated
Sep 30, 2016
Renaming things
#35
· opened
Sep 29, 2016
by
Ralf Jung
Iris 3.0
CLOSED
42
updated
Nov 09, 2016
STSs: Consider changing the def. of frame-steps
#36
· opened
Sep 29, 2016
by
Ralf Jung
A-theory
C-project
T-algebra
CLOSED
5
updated
Nov 01, 2019
saved_prop for predicate
#37
· opened
Oct 05, 2016
by
Ghost User
CLOSED
8
updated
Oct 05, 2016
Refactor bigops
#38
· opened
Oct 10, 2016
by
Ralf Jung
CLOSED
1
4
updated
Apr 01, 2017
iIntros: bad error when trying to use a name that's already used
#39
· opened
Oct 26, 2016
by
Ralf Jung
T-proofmode
CLOSED
1
updated
Oct 26, 2016
iRewrite and internal equality on predicates
#40
· opened
Oct 27, 2016
by
Janno
CLOSED
4
updated
Oct 27, 2016
Prev
1
2
3
4
5
6
…
20
Next