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}}
Created date
Add LICENSE, following the Iris LICENSE file.
ora!1
· created
Mar 13, 2020
by
Robbert Krebbers
Merged
4
updated
Apr 09, 2020
Add LICENSE file.
6 of 6 checklist items completed
tutorial-popl18!3
· created
Mar 13, 2020
by
Robbert Krebbers
Merged
9
updated
Mar 14, 2020
fill in blanks in LICENSE
lambda-rust!16
· created
Mar 13, 2020
by
Ralf Jung
masters/weak_mem
Merged
1
updated
Mar 14, 2020
fill in blanks in LICENSE
gpfsl!3
· created
Mar 13, 2020
by
Ralf Jung
Merged
1
updated
Mar 14, 2020
fill in blanks in LICENSE
lambda-rust!15
· created
Mar 13, 2020
by
Ralf Jung
Merged
2
updated
Mar 14, 2020
fill in blanks in LICENSE
examples!31
· created
Mar 13, 2020
by
Ralf Jung
Merged
2
updated
Mar 14, 2020
Remove copyright headers, update LICENCE file.
stdpp!124
· created
Mar 13, 2020
by
Robbert Krebbers
Merged
3
updated
Mar 13, 2020
Close issue #299: `leibnizO` finds convoluted proof for definitions
iris!392
· created
Mar 12, 2020
by
Robbert Krebbers
Merged
1
6
updated
Mar 12, 2020
Testcase for https://gitlab.mpi-sws.org/iris/stdpp/merge_requests/123.
iris!391
· created
Mar 10, 2020
by
Robbert Krebbers
Merged
0
updated
Mar 10, 2020
Change mode of `TCEq`.
stdpp!123
· created
Mar 10, 2020
by
Robbert Krebbers
Merged
1
updated
Oct 06, 2023
Avoid using Hint Resolve with a term
iris!390
· created
Mar 10, 2020
by
Tej Chajed
Merged
0
updated
Mar 10, 2020
Avoid using Hint Resolve with a term
stdpp!122
· created
Mar 10, 2020
by
Tej Chajed
Merged
7
updated
Mar 10, 2020
More consistent names for `fill` lemmas of `LanguageCtx`.
iris!389
· created
Mar 09, 2020
by
Robbert Krebbers
Merged
9
updated
Mar 10, 2020
prove later commuting around equality one way
iris!388
· created
Mar 06, 2020
by
Ralf Jung
Merged
11
updated
Mar 15, 2020
Set `Hint Mode` for logical `TCX` type classes
stdpp!121
· created
Mar 06, 2020
by
Robbert Krebbers
Merged
4
updated
Mar 10, 2020
Rename `fin_of_nat` → `nat_to_fin` to follow the conventions.
stdpp!120
· created
Mar 05, 2020
by
Robbert Krebbers
Merged
1
updated
Mar 05, 2020
fill in blanks in license
iris!387
· created
Mar 04, 2020
by
Ralf Jung
Merged
21
updated
Mar 13, 2020
no longer reftest old Coq 8.9
iris!386
· created
Feb 28, 2020
by
Ralf Jung
Merged
1
updated
Feb 28, 2020
slightly expand notation docs
iris!385
· created
Feb 26, 2020
by
Ralf Jung
Merged
3
updated
Feb 26, 2020
Add a weakening lemma for goals: "is_Some (<[i:=x]>m !! j)"
stdpp!119
· created
Feb 26, 2020
by
Armaël Guéneau
Closed
3
updated
Feb 26, 2020
Prev
1
…
69
70
71
72
73
74
75
76
77
…
101
Next