Skip to content
GitLab
Explore
Sign in
Iris
Merge requests
Open
47
Merged
1,756
Closed
208
All
2,011
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
add locality annotation to all Typeclasses Opaque/Transparent
iris!918
· created
May 02, 2023
by
Ralf Jung
Merged
5
updated
May 03, 2023
use more primitive projections in cmra.v
iris!919
· created
May 02, 2023
by
Ralf Jung
Merged
8
updated
May 02, 2023
Make projections of BI operational type classes `Typeclasses Opaque`.
iris!914
· created
Apr 28, 2023
by
Robbert Krebbers
Merged
8
updated
May 02, 2023
Make `union_Some` a `↔`, add `union_None` and `union_is_Some`.
stdpp!472
· created
May 01, 2023
by
Robbert Krebbers
Merged
5
updated
May 02, 2023
Drop support for Coq 8.14.
stdpp!468
· created
Apr 24, 2023
by
Robbert Krebbers
Merged
2
updated
May 01, 2023
Also put results about `N` in a module.
stdpp!465
· created
Apr 22, 2023
by
Robbert Krebbers
Merged
2
updated
May 01, 2023
Set `simpl never` for `Pos` and `N`.
stdpp!464
· created
Apr 22, 2023
by
Robbert Krebbers
Merged
2
updated
May 01, 2023
Let compilation under Coq 8.17 succeed without warnings.
stdpp!469
· created
Apr 24, 2023
by
Robbert Krebbers
Merged
3
updated
Apr 30, 2023
Bump stdpp
iris!915
· created
Apr 29, 2023
by
Lennard Gäher
Merged
0
updated
Apr 30, 2023
Make `persistently_True` a bi-entailment.
iris!912
· created
Apr 27, 2023
by
Robbert Krebbers
Merged
3
updated
Apr 28, 2023
Remove `left associativity` of `scalar_mult` to be compatible with math-comp.
stdpp!470
· created
Apr 28, 2023
by
Robbert Krebbers
Merged
0
updated
Apr 28, 2023
drop support for Coq 8.14
iris!908
· created
Apr 24, 2023
by
Ralf Jung
Merged
1
updated
Apr 28, 2023
Make `BiLaterContractive` a class instead of a notation.
iris!913
· created
Apr 28, 2023
by
Robbert Krebbers
Merged
1
updated
Apr 28, 2023
Generalize `intuitionistically_intro` to general BI.
iris!911
· created
Apr 27, 2023
by
Robbert Krebbers
Merged
1
updated
Apr 27, 2023
Restructure derived_laws of BI
iris!909
· created
Apr 25, 2023
by
Robbert Krebbers
Merged
1
updated
Apr 26, 2023
Consistently write `TCOr (Affine ..) (Absorbing ..)` instead of the other way around.
iris!910
· created
Apr 25, 2023
by
Robbert Krebbers
Merged
1
updated
Apr 25, 2023
Strenghten `cmra_valid_elim` and derive `cmra_valid_discrete`.
iris!902
· created
Mar 26, 2023
by
Robbert Krebbers
Merged
5
updated
Apr 24, 2023
add mono_Z base-logic library
iris!880
· created
Dec 22, 2022
by
Ralf Jung
Merged
4
updated
Apr 24, 2023
Add `max_Z`/`mono_Z` camera
iris!889
· created
Feb 08, 2023
by
Robbert Krebbers
Merged
11
updated
Apr 24, 2023
Compatibility lemma between big_sepM and big_sepL2 with map_to_list
iris!901
· created
Mar 22, 2023
by
Dorian Lesbre
Merged
11
updated
Apr 24, 2023
Prev
1
…
10
11
12
13
14
15
16
17
18
…
88
Next