Merge requests · Iris / Iris

Draft: Improve validity information received from `iCombine`ing `own`s

!930 · created May 25, 2023 by Ike Mulder
S-postponed
- Closed
- 25
updated Feb 12, 2025
add fixpoint lemmas for plain and absorbing

!903 · created Apr 01, 2023 by William Mansky
- Closed
- 21
updated Feb 07, 2025
Allow controlling stuckness at the language level 0 of 6 checklist items completed

!825 · created Aug 02, 2022 by Michael Sammler
S-postponed
- Closed
- 60
updated Feb 07, 2025
WIP: Step Update modality demonstration

!887 · created Jan 30, 2023 by Jonas Kastberg
- Closed
- 2
- 1
updated Feb 07, 2025
Improve lc support for iNext and wp_pure

!1099 · created Feb 05, 2025 by ffengyu
- Closed
updated Feb 05, 2025
`Unify` type class that factors out use of `notypeclasses refine` in proof mode classes.

!916 · created Apr 30, 2023 by Robbert Krebbers
S-waiting-for-author
- Closed
- 7
updated Oct 10, 2024
Fix notation-related warnings on Coq 8.20

!1074 · created Sep 11, 2024 by Tej Chajed
- Closed
- 3
updated Sep 11, 2024
Promise 8.20 compatibility

!1075 · created Sep 11, 2024 by Tej Chajed
- Closed
- 1
updated Sep 11, 2024
Enable `Typeclasses Strict Resolution` for dervied_connectives.v 0 of 1 checklist item completed

!642 · created Feb 19, 2021 by Janno
- Closed
- 15
updated Aug 16, 2024
Make bi polymorphic in logic and quant universes

!1058 · created Jul 22, 2024 by Tej Chajed
- Closed
- 40
updated Aug 15, 2024
Renamed/added macros to iris.sty

!851 · created Oct 12, 2022 by Jonas Kastberg
S-waiting-for-author
- Closed
- 39
updated Jul 30, 2024
Draft: Coq 18928

!1046 · created Apr 16, 2024 by Pierre Roux
- Closed
- 3
updated Apr 16, 2024
Add lemmas for creating later credits for non-pure steps.

!1034 · created Feb 22, 2024 by tlsomers
- Closed
- 6
updated Mar 06, 2024
WIP: Strong framing

!50 · created Feb 18, 2017 by Robbert Krebbers
T-proofmode
- Closed
- 31
updated Feb 13, 2024
Bump version of stdpp

!1021 · created Nov 17, 2023 by Pierre Rousselin
- Closed
- 8
updated Nov 17, 2023
Adapt to https://github.com/coq/coq/pull/18014

!1009 · created Oct 19, 2023 by Pierre Roux
- Closed
- 4
updated Oct 21, 2023
Simplify NA-inv protocol.

!1000 · created Oct 06, 2023 by Jacques-Henri Jourdan
- Closed
- 17
updated Oct 17, 2023
Fixed iFrame under ∧ and ∨ taking forever to fail in the presence of evars, alternative

!991 · created Sep 28, 2023 by Ike Mulder
- Closed
- 3
updated Oct 10, 2023
Draft: Add simple library for priority levels and use it for `iFrame`

!742 · created Oct 11, 2021 by Robbert Krebbers
S-waiting-for-author
- Closed
- 18
updated Sep 29, 2023
Make* class tweaks

!842 · created Aug 13, 2022 by Ralf Jung
S-blocked
- Closed
- 40
updated Jul 25, 2023