Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
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
iris.sty incompatible with acmart
#335
· opened
Jul 14, 2020
by
Ralf Jung
A-docs
C-bug
6
updated
Jul 15, 2020
Expand test coverage of proofmode
0 of 3 tasks completed
#334
· opened
Jul 13, 2020
by
Tej Chajed
A-coq
C-enhancement
T-proofmode
1
updated
Jul 14, 2020
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
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
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
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
Choose syntax and implement destructuring existentials with pure components, following !400
0 of 3 tasks completed
#310
· opened
Apr 17, 2020
by
Paolo G. Giarrusso
A-coq
C-enhancement
T-proofmode
1
1
10
updated
Jul 22, 2020
Automatically enforce use of Unicode → instead of ASCII ->
#308
· opened
Apr 07, 2020
by
Tej Chajed
A-coq
C-enhancement
T-style
1
8
updated
Apr 16, 2020
Direction of _op lemmas is inconsistent with _(p)core, _valid, _included
#304
· opened
Apr 06, 2020
by
Ralf Jung
A-coq
C-enhancement
T-algebra
2
updated
Apr 06, 2020
Canonical structures have major performance impact
#303
· opened
Apr 05, 2020
by
Robbert Krebbers
A-coq
C-enhancement
I-performance
T-bi
17
updated
May 11, 2020
vs doesn't use FUpd
#300
· opened
Mar 28, 2020
by
Gregory Malecha
A-coq
C-enhancement
T-base_logic
T-bi
4
updated
Mar 30, 2020
Guide typeclass search via more specialized typeclasses
#298
· opened
Mar 06, 2020
by
Michael Sammler
A-coq
C-enhancement
I-performance
2
updated
Jun 17, 2020
Persistent (and other BI class) instances missing for telescopes
#297
· opened
Mar 05, 2020
by
Robbert Krebbers
A-coq
C-enhancement
T-bi
0
updated
Mar 05, 2020
Have iApply introduce equalities for subterms that cannot be unified directly
#295
· opened
Feb 24, 2020
by
Armaël Guéneau
A-coq
C-enhancement
T-proofmode
1
4
updated
Aug 08, 2020
Possible redesign of handling of persistent/intuitionistic propositions in intro patterns
#290
· opened
Feb 11, 2020
by
Ralf Jung
A-coq
C-enhancement
T-proofmode
1
updated
Feb 11, 2020
Prev
1
2
3
4
5
6
7
Next