Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Support
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
I
Iris
Group overview
Group overview
Details
Activity
Issues
155
Issues
155
List
Board
Labels
Milestones
Merge Requests
21
Merge Requests
21
Members
Members
Collapse sidebar
Close sidebar
Open sidebar
Iris
Issues
Open
155
Closed
287
All
442
Recent searches
{{formattedKey}}
{{ title }}
{{ help }}
{{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
Iris Library Best Practices
iris#333
· opened
Jul 07, 2020
by
Ralf Jung
A-docs
1
0
updated
Jul 07, 2020
Become part of Coq Platform?
iris#332
· opened
Jul 05, 2020
by
Ralf Jung
3
4
updated
Jul 05, 2020
Consider switching from simpl to cbn
stdpp#74
· opened
Jul 02, 2020
by
Paolo G. Giarrusso
6
updated
Jul 02, 2020
Add `add_hypothesis`-like tactic
stdpp#73
· opened
Jun 29, 2020
by
Robbert
4
updated
Jun 29, 2020
simpl breaks error checking of `iNext (S i)`
iris#331
· opened
Jun 29, 2020
by
Paolo G. Giarrusso
1
3
updated
Jun 29, 2020
Have a single version that works across Coq 8.11 and 8.12
string-ident#3
· opened
Jun 26, 2020
by
Ralf Jung
0
updated
Jun 26, 2020
Consider adding `iEnough` variants of `iAssert` ?
iris#330
· opened
Jun 25, 2020
by
Paolo G. Giarrusso
A-coq
C-enhancement
T-proofmode
3
updated
Jun 26, 2020
Iris Website Reform
iris#329
· opened
Jun 25, 2020
by
Ralf Jung
A-infra
A-meta
C-project
2
1
updated
Jun 25, 2020
Add list_to_imap and associated theory
stdpp#71
· opened
Jun 24, 2020
by
Tej Chajed
0
updated
Jun 24, 2020
Add pattern variant of bind notation
stdpp#70
· opened
Jun 23, 2020
by
Paolo G. Giarrusso
1
7
updated
Jul 01, 2020
Add RA for auth of a heap
iris#328
· opened
Jun 23, 2020
by
Ralf Jung
A-coq
C-enhancement
T-algebra
1
updated
Jun 23, 2020
Add RA for auth max_nat
iris#327
· opened
Jun 19, 2020
by
Robbert
2
0
updated
Jun 19, 2020
Add an overview of important classes, theorems, and notations
stdpp#69
· opened
Jun 18, 2020
by
Tej Chajed
1
2
updated
Jun 18, 2020
finite_countable Hint Immediate in typeclass_instances is broken
stdpp#68
· opened
Jun 04, 2020
by
Tej Chajed
5
updated
Jun 04, 2020
Make `contractive_proper` into a lemma, or control other instances that make it costly.
iris#321
· opened
May 27, 2020
by
Paolo G. Giarrusso
1
0
updated
May 27, 2020
λne should use %I for body — or add a variant using `%I`.
iris#320
· opened
May 27, 2020
by
Paolo G. Giarrusso
4
updated
May 27, 2020
Rules for deallocation
reloc#8
· opened
May 26, 2020
by
Dan Frumin
0
updated
May 26, 2020
Better documentation for sets
stdpp#66
· opened
May 25, 2020
by
Tej Chajed
0
updated
May 25, 2020
Weird unfolding by `cbn` with `gset`
stdpp#65
· opened
May 22, 2020
by
Rodolphe Lepigre
2
updated
May 25, 2020
Further issues with in-Coq computation for pmap and gmap
stdpp#64
· opened
May 20, 2020
by
Paolo G. Giarrusso
0
updated
May 20, 2020
Prev
1
2
3
4
5
…
8
Next
1
