Skip to content
GitLab
Explore
Sign in
Iris
Merge requests
Open
49
Merged
1,756
Closed
208
All
2,013
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}}
{{title}}
Updated date
Let `iProp` refer to `uPred ... : Type` instead of `uPredO ... : ofeT`
iris!314
· created
Sep 16, 2019
by
Robbert Krebbers
Merged
10
updated
Sep 19, 2019
Fix w.r.t. coq/coq#10764.
stdpp!98
· created
Sep 19, 2019
by
Ghost User
Merged
2
updated
Sep 19, 2019
Add `iStopProof` tactic
iris!311
· created
Sep 07, 2019
by
Robbert Krebbers
Merged
1
8
updated
Sep 19, 2019
Generalize `list_find` lemmas to become bi-implications.
stdpp!99
· created
Oct 01, 2019
by
Robbert Krebbers
Merged
0
updated
Oct 07, 2019
Prove that non-value WP is contractive.
iris!316
· created
Oct 07, 2019
by
Robbert Krebbers
Merged
5
updated
Oct 11, 2019
Add `Atomic` instances for all atomic `heap_lang` constructs.
iris!317
· created
Oct 12, 2019
by
Robbert Krebbers
Merged
1
6
updated
Oct 14, 2019
rename LitErased -> LitPoison
iris!318
· created
Oct 31, 2019
by
Ralf Jung
Merged
0
updated
Nov 01, 2019
Documentation for #237
iris!234
· created
Apr 15, 2019
by
Paolo G. Giarrusso
Merged
13
updated
Nov 01, 2019
Allow swapping later^n and forall
iris!221
· created
Mar 03, 2019
by
Paolo G. Giarrusso
Merged
9
updated
Nov 01, 2019
drop Coq 8.7 and add 8.10
iris!320
· created
Nov 01, 2019
by
Ralf Jung
Merged
0
updated
Nov 01, 2019
Update version in URL for Iris appendix
iris!321
· created
Nov 01, 2019
by
Paolo G. Giarrusso
Merged
1
updated
Nov 01, 2019
Add two useful lemmas
stdpp!101
· created
Oct 31, 2019
by
Amin Timany
Merged
5
updated
Nov 01, 2019
make gFunctors_lookup a local coercion to avoid ambiguous paths
iris!322
· created
Nov 01, 2019
by
Ralf Jung
Merged
0
updated
Nov 01, 2019
Add congruence lemmas for closures
stdpp!102
· created
Nov 01, 2019
by
Amin Timany
Merged
0
updated
Nov 01, 2019
move docs around
iris!323
· created
Nov 01, 2019
by
Ralf Jung
Merged
0
updated
Nov 01, 2019
Update gitignore for compatibility with Coq master
iris!325
· created
Nov 01, 2019
by
Tej Chajed
Merged
1
updated
Nov 02, 2019
Update gitignore for compatibility with Coq master
stdpp!103
· created
Nov 01, 2019
by
Tej Chajed
Merged
1
updated
Nov 02, 2019
Semantic invariants
iris!319
· created
Nov 01, 2019
by
Ralf Jung
Merged
1
updated
Nov 05, 2019
Simplify definition of invariant model.
iris!327
· created
Nov 05, 2019
by
Robbert Krebbers
Merged
3
updated
Nov 05, 2019
Added a stronger version of cinv_open_strong
iris!326
· created
Nov 04, 2019
by
Jonas Kastberg
Merged
21
updated
Nov 05, 2019
Prev
1
…
14
15
16
17
18
19
20
21
22
…
88
Next