Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Support
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
I
Iris
Group overview
Group overview
Details
Activity
Issues
114
Issues
114
List
Board
Labels
Milestones
Merge Requests
10
Merge Requests
10
Members
Members
Collapse sidebar
Close sidebar
Open sidebar
Iris
Issues
Open
114
Closed
243
All
357
Recent searches
Press Enter or click to search
{{hint}}
{{tag}}
{{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}}
Created date
Priority
Created date
Last updated
Milestone due date
Due date
Popularity
Label priority
Manual
Remove eta-expansions from sealed definitions
iris#285
· opened
Jan 15, 2020
by
Ralf Jung
A-coq
C-enhancement
T-style
0
updated
Jan 15, 2020
Undesired simplification behaviour of big_sepM2
iris#282
· opened
Dec 20, 2019
by
Michael Sammler
A-coq
C-bug
T-bi
5
updated
Dec 27, 2019
Documentation for installation on OS X
iris#280
· opened
Dec 16, 2019
by
Jules Jacobs
A-docs
C-enhancement
1
8
updated
Dec 17, 2019
Editor config for Emacs should include the bindings in the m17n configuration
iris#279
· opened
Dec 14, 2019
by
Tej Chajed
A-docs
C-enhancement
2
updated
Dec 16, 2019
Write `wp_` lemmas for array operations in a more `iApply`/`wp_apply` friendly way
iris#278
· opened
Dec 09, 2019
by
Ralf Jung
A-coq
C-bug
T-heap_lang
4
updated
Dec 12, 2019
solve_ndisj taking a long time
stdpp#47
· opened
Dec 03, 2019
by
Jonas Kastberg
1
updated
Dec 04, 2019
Find a way to reduce usage of O/R/U suffixes
iris#277
· opened
Dec 02, 2019
by
Ralf Jung
A-coq
C-enhancement
T-algebra
0
updated
Dec 02, 2019
Create example user library
iris#276
· opened
Dec 02, 2019
by
Robbert
A-docs
C-enhancement
T-style
0
updated
Dec 02, 2019
use implicit arguments for lemmas in coq_tactics.v
0 of 1 task completed
iris#275
· opened
Nov 22, 2019
by
Paolo G. Giarrusso
A-coq
C-enhancement
T-proofmode
0
updated
Nov 22, 2019
Iris shadows ssreflect new syntax
iris#273
· opened
Nov 07, 2019
by
Paolo G. Giarrusso
A-coq
C-bug
T-algebra
15
updated
Nov 22, 2019
Fix performance regressions in Iris and std++ in Coq 8.10.1 compared to Coq 8.9.0
iris#272
· opened
Nov 07, 2019
by
Robbert
A-coq
I-performance
8
updated
Jan 14, 2020
Follow-up from "Lang lemmas": intuitive explanation of mixin_step_by_val
iris#271
· opened
Nov 06, 2019
by
Ralf Jung
A-theory
C-enhancement
T-heap_lang
0
updated
Nov 06, 2019
non-Unicode Iris notations
iris#270
· opened
Nov 01, 2019
by
Ralf Jung
A-coq
C-enhancement
T-style
27
updated
Jan 16, 2020
Provide a proof of the vec_to_list correspondence.
stdpp#45
· opened
Oct 27, 2019
by
Tiago Campos
0
updated
Oct 27, 2019
Editor config should explain how to configure CoqIDE 8.10 unicode input
iris#269
· opened
Oct 19, 2019
by
Tej Chajed
A-docs
C-enhancement
1
1
updated
Dec 14, 2019
`iInv` with cancellable invariants and a cinv_own token
iris#268
· opened
Sep 30, 2019
by
Dan Frumin
A-coq
C-enhancement
T-proofmode
1
updated
Nov 01, 2019
Inconsistent order of arguments for `inv_alloc` and `cinv_alloc`.
iris#267
· opened
Sep 30, 2019
by
Dan Frumin
A-coq
C-bug
T-base_logic
T-style
2
updated
Nov 01, 2019
`Hint Mode` for `QuoteLookup` and `Quote`
stdpp#44
· opened
Sep 16, 2019
by
Dan Frumin
4
updated
Sep 19, 2019
Provide a total version of `!!` for finite maps and lists
stdpp#43
· opened
Sep 16, 2019
by
Robbert
7
updated
Nov 17, 2019
Investigate use of "Filtered Unification"
iris#264
· opened
Aug 31, 2019
by
Ralf Jung
A-coq
C-project
0
updated
Nov 01, 2019
Prev
1
2
3
4
5
…
Next
Last »
1