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
drop support for Coq 8.12 and 8.13
stdpp!440
· created
Jan 09, 2023
by
Ralf Jung
Merged
2
updated
Apr 24, 2023
Use `positive` in `gmultiset` representation to avoid off-by-one computations.
stdpp!463
· created
Apr 19, 2023
by
Robbert Krebbers
Merged
2
updated
Apr 24, 2023
Add lemma `map_zip_fst_snd`.
stdpp!467
· created
Apr 24, 2023
by
Robbert Krebbers
Merged
0
updated
Apr 24, 2023
Rename plus/minus → add/sub and put number lemmas in modules to be consistent with Coq stdlib
stdpp!404
· created
Aug 08, 2022
by
Robbert Krebbers
Merged
33
updated
Apr 22, 2023
slightly generalize and reorganize fupd soundness lemmas
iris!863
· created
Nov 13, 2022
by
Ralf Jung
Merged
24
updated
Apr 19, 2023
Add `min` and `max` infix notations for `positive`.
stdpp!462
· created
Apr 19, 2023
by
Robbert Krebbers
Merged
1
updated
Apr 19, 2023
Use `SProp` to obtain better definitional equality for `pmap`, `gmap`, `gset`, `Qp`, and `coPset`
stdpp!309
· created
Jul 27, 2021
by
Robbert Krebbers
Merged
45
updated
Apr 18, 2023
Add NoDup_bind, vec_enum, vec_finite (new version with proper branch)
stdpp!458
· created
Mar 24, 2023
by
Robbert Krebbers
Merged
1
updated
Apr 18, 2023
Add set_omap to finite sets
stdpp!456
· created
Mar 20, 2023
by
Dorian Lesbre
Merged
8
updated
Apr 18, 2023
add some union_with lemmas
stdpp!432
· created
Dec 13, 2022
by
Ralf Jung
Merged
27
updated
Apr 14, 2023
bugfix for persistent auto frame in specialization pattern
iris!906
· created
Apr 12, 2023
by
Yixuan Chen
Merged
5
updated
Apr 12, 2023
Use `eauto` as default for `set_solver`.
stdpp!420
· created
Oct 24, 2022
by
Robbert Krebbers
Merged
11
updated
Apr 12, 2023
Add support for Coq version 8.17.0.
iris!904
· created
Apr 03, 2023
by
Rodolphe Lepigre
Merged
12
updated
Apr 11, 2023
Extend `set_solver` with support for `set_Forall` and `set_Exists`.
stdpp!460
· created
Apr 11, 2023
by
Robbert Krebbers
Merged
2
updated
Apr 11, 2023
Enable CI for Coq 8.17.0.
iris!905
· created
Apr 06, 2023
by
Rodolphe Lepigre
Merged
1
updated
Apr 11, 2023
add note in developers.md for mlgmpidl library and small corrections in the annotations docs
refinedc!143
· created
Apr 04, 2023
by
Kimaya Bedarkar
Merged
1
updated
Apr 04, 2023
Add some list lemmas
stdpp!441
· created
Jan 10, 2023
by
Ralf Jung
Merged
1
35
updated
Mar 24, 2023
miscellaneous map lemmas
stdpp!442
· created
Jan 10, 2023
by
Ralf Jung
Merged
18
updated
Mar 24, 2023
Rename `option_union_Some` → `union_Some`
stdpp!449
· created
Feb 17, 2023
by
Robbert Krebbers
Merged
1
updated
Mar 21, 2023
Various tweaks to lists, maps, sets
stdpp!455
· created
Mar 19, 2023
by
Robbert Krebbers
Merged
19
updated
Mar 21, 2023
Prev
1
…
11
12
13
14
15
16
17
18
19
…
88
Next