Skip to content
GitLab
Explore
Sign in
Iris
Merge requests
Open
49
Merged
1,743
Closed
206
All
1,998
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
Revert "Merge branch 'ralf/separable' into 'master'"
iris!924
· created
May 05, 2023
by
Ralf Jung
Merged
9
updated
May 05, 2023
re-export std++ options
iris!922
· created
May 04, 2023
by
Ralf Jung
Merged
2
updated
May 05, 2023
Better handling of `let` bindings in proof mode
iris!921
· created
May 04, 2023
by
Robbert Krebbers
Merged
8
updated
May 05, 2023
Simplify definition of `mapset_dom_with`.
stdpp!476
· created
May 04, 2023
by
Robbert Krebbers
Merged
3
updated
May 04, 2023
More canonical maps
stdpp!461
· created
Apr 18, 2023
by
Robbert Krebbers
Merged
1
24
updated
May 04, 2023
make Prop-level BI connectives notation for bi_emp_valid (rather than bi_entails)
iris!791
· created
May 07, 2022
by
Ralf Jung
Merged
44
updated
May 03, 2023
add locality annotation to all Typeclasses Opaque/Transparent
iris!918
· created
May 02, 2023
by
Ralf Jung
Merged
5
updated
May 03, 2023
Take advantage of new Coq features in Coq 8.15
stdpp!473
· created
May 01, 2023
by
Robbert Krebbers
Merged
9
updated
May 02, 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
Prev
1
…
9
10
11
12
13
14
15
16
17
…
88
Next