Skip to content
GitLab
Explore
Sign in
Iris
Iris
Merge requests
Open
19
Merged
909
Closed
118
All
1,046
Actions
Subscribe to RSS feed
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
Fix bug in `iApply` prettification.
!788
· created
Apr 20, 2022
by
Robbert Krebbers
Merged
1
2
updated
May 01, 2022
Dump `siProp_scope` and use `bi_scope`. This is consistent with `uPred`.
!786
· created
Apr 07, 2022
by
Robbert Krebbers
Merged
15
updated
Apr 08, 2022
Ensure that different `Cofe` proofs of `iProp` are convertible.
!784
· created
Mar 30, 2022
by
Robbert Krebbers
Merged
6
updated
Apr 07, 2022
Use |-@{...} to avoid the need for casts (in tests)
!785
· created
Apr 07, 2022
by
Gregory Malecha
Merged
3
updated
Apr 07, 2022
GFunctors changed to a record
!782
· created
Mar 17, 2022
by
Irene Yoon
Merged
1
32
updated
Mar 18, 2022
Prevent cbn from unfolding the 'heap_lang' term.
!779
· created
Feb 21, 2022
by
Ike Mulder
Merged
14
updated
Feb 23, 2022
Extend `iInduction` with support for induction schemes containing `Forall`.
!731
· created
Sep 03, 2021
by
Robbert Krebbers
Merged
22
updated
Feb 11, 2022
big_op: weaken all Absorbing conditions using TCOr and Affine
!757
· created
Nov 26, 2021
by
Glen Mével
Merged
48
updated
Feb 02, 2022
Stop `iAssumption` from unifying evar premises with `False`
!772
· created
Jan 13, 2022
by
Janno
Merged
16
updated
Jan 24, 2022
Iris 3.6.0 release notes
!777
· created
Jan 20, 2022
by
Tej Chajed
Merged
9
updated
Jan 23, 2022
unstage mono_list algebra
!761
· created
Nov 29, 2021
by
Ralf Jung
Merged
7
updated
Jan 17, 2022
mono_nat algebra: add dfrac support and notation
!759
· created
Nov 29, 2021
by
Ralf Jung
Merged
12
updated
Jan 17, 2022
don't make frame_fractional an instance
!739
· created
Oct 01, 2021
by
Ralf Jung
Merged
20
updated
Jan 17, 2022
remove auth_frac_op lemmas
!774
· created
Jan 15, 2022
by
Ralf Jung
Merged
1
updated
Jan 17, 2022
rename the new dfrac_agree update lemmas for consistency
!769
· created
Dec 17, 2021
by
Ralf Jung
Merged
1
5
updated
Jan 15, 2022
Fix bi_rewrite_relation hint priority
!773
· created
Jan 14, 2022
by
Matthieu Sozeau
Merged
25
updated
Jan 14, 2022
Formulate `is_closed_expr` in terms of `gset`s.
!707
· created
Jun 20, 2021
by
Dan Frumin
Merged
39
updated
Jan 11, 2022
Fix name, `Later_inj` -> `Next_inj`.
!770
· created
Dec 28, 2021
by
Dan Frumin
Merged
1
2
updated
Dec 30, 2021
simplify telescope-based notations
!762
· created
Nov 30, 2021
by
Ralf Jung
Merged
2
updated
Dec 17, 2021
drop support for Coq 8.12
!763
· created
Dec 04, 2021
by
Ralf Jung
Merged
1
3
updated
Dec 17, 2021
Prev
1
…
9
10
11
12
13
14
15
16
17
…
46
Next