Skip to content
GitLab
Explore
Sign in
Iris
Merge requests
Open
50
Merged
1,756
Closed
208
All
2,014
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
Make `BiLaterContractive` a class instead of a notation.
iris!913
· created
Apr 28, 2023
by
Robbert Krebbers
Merged
1
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
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
Make `persistently_True` a bi-entailment.
iris!912
· created
Apr 27, 2023
by
Robbert Krebbers
Merged
3
updated
Apr 28, 2023
Bump stdpp
iris!915
· created
Apr 29, 2023
by
Lennard Gäher
Merged
0
updated
Apr 30, 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
Set `simpl never` for `Pos` and `N`.
stdpp!464
· created
Apr 22, 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
Drop support for Coq 8.14.
stdpp!468
· created
Apr 24, 2023
by
Robbert Krebbers
Merged
2
updated
May 01, 2023
Enable `Hint Mode Equiv` now that stdpp requires Coq 8.12
stdpp!437
· created
Dec 16, 2022
by
Paolo G. Giarrusso
Closed
7
updated
May 02, 2023
Draft: Fix #497: avoid Hint Immediate
iris!869
· created
Nov 24, 2022
by
Paolo G. Giarrusso
S-blocked
Closed
1
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
Prevent [finite_countable] from solving unrelated evars
1 of 4 checklist items completed
stdpp!424
· created
Nov 24, 2022
by
Paolo G. Giarrusso
Closed
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
use more primitive projections in cmra.v
iris!919
· created
May 02, 2023
by
Ralf Jung
Merged
8
updated
May 02, 2023
add locality annotation to all Typeclasses Opaque/Transparent
iris!918
· created
May 02, 2023
by
Ralf Jung
Merged
5
updated
May 03, 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
More canonical maps
stdpp!461
· created
Apr 18, 2023
by
Robbert Krebbers
Merged
1
24
updated
May 04, 2023
Simplify definition of `mapset_dom_with`.
stdpp!476
· created
May 04, 2023
by
Robbert Krebbers
Merged
3
updated
May 04, 2023
Better handling of `let` bindings in proof mode
iris!921
· created
May 04, 2023
by
Robbert Krebbers
Merged
8
updated
May 05, 2023
Prev
1
…
81
82
83
84
85
86
87
88
89
…
101
Next