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}}
Closed date
Rename seal lemmas from `_eq` to `_unseal` and make sealing stuff `Local`.
stdpp!378
· created
May 12, 2022
by
Robbert Krebbers
Merged
15
updated
May 13, 2022
drop support for Coq 8.11
stdpp!377
· created
May 09, 2022
by
Ralf Jung
Merged
2
updated
May 11, 2022
First Steps for Later Credits
iris!792
· created
May 09, 2022
by
Simon Spies
Merged
221
updated
Jul 05, 2022
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
make dom domain type paremeter (D) implicit
stdpp!376
· created
May 07, 2022
by
Ralf Jung
Merged
15
updated
May 19, 2022
Bump stdpp to include telescope fixes
iris!790
· created
May 04, 2022
by
Paolo G. Giarrusso
Merged
0
updated
May 04, 2022
Annotate telescope notations to support literal telescope arguments.
stdpp!375
· created
May 03, 2022
by
Janno
Merged
12
updated
May 04, 2022
add and verify simpler bitmap implementation
refinedc!135
· created
May 02, 2022
by
Kimaya Bedarkar
ci/example-scheduler
Merged
Approved
1
updated
May 03, 2022
Let `iRevert` of a pure hypotheses generate a wand instead of implication.
iris!789
· created
Apr 23, 2022
by
Robbert Krebbers
Merged
3
updated
May 08, 2024
Fix bug in `iApply` prettification.
iris!788
· created
Apr 20, 2022
by
Robbert Krebbers
Merged
1
2
updated
May 01, 2022
add big_sepS_insert_2' and big_sepS_union_2
iris!787
· created
Apr 16, 2022
by
Ralf Jung
Merged
3
updated
May 09, 2022
Add induction principle for `tele_arg`.
stdpp!374
· created
Apr 12, 2022
by
Robbert Krebbers
Merged
1
updated
Apr 12, 2022
Add Pigeon Hole principle.
stdpp!373
· created
Apr 11, 2022
by
Robbert Krebbers
Merged
7
updated
Apr 12, 2022
Dump `siProp_scope` and use `bi_scope`. This is consistent with `uPred`.
iris!786
· created
Apr 07, 2022
by
Robbert Krebbers
Merged
15
updated
Apr 08, 2022
Use |-@{...} to avoid the need for casts (in tests)
iris!785
· created
Apr 07, 2022
by
Gregory Malecha
Merged
3
updated
Apr 07, 2022
Ensure that different `Cofe` proofs of `iProp` are convertible.
iris!784
· created
Mar 30, 2022
by
Robbert Krebbers
Merged
6
updated
Apr 07, 2022
Clarify relationship between `gset_to_gmap` and `set_to_map`.
stdpp!371
· created
Mar 30, 2022
by
Robbert Krebbers
Merged
2
updated
Apr 07, 2022
Added capability for stripping multiple laters per step in HeapLang
iris!783
· created
Mar 22, 2022
by
Jonas Kastberg
Merged
50
updated
Aug 14, 2022
Removed `skipN` instruction in `send` implementation
actris!26
· created
Mar 22, 2022
by
Jonas Kastberg
Merged
0
updated
Apr 19, 2022
GFunctors changed to a record
iris!782
· created
Mar 17, 2022
by
Irene Yoon
Merged
1
32
updated
Mar 18, 2022
Prev
1
…
20
21
22
23
24
25
26
27
28
…
88
Next