Merge requests · Iris / Iris · GitLab

Make `iFrame` fail if more work remains

!1094 · created Nov 24, 2024 by Robbert Krebbers
- 11
updated Dec 09, 2024
Draft: Custom intro patterns

!1093 · created Nov 24, 2024 by clef-men
- 5
- 1
updated Nov 25, 2024
Support arbitrary string types in IPM tactics

!1090 · created Nov 12, 2024 by Janno
- 26
updated Dec 05, 2024
Use `refine` for `Frame` base cases.

!1082 · created Oct 08, 2024 by Robbert Krebbers
- 15
updated Oct 10, 2024
Remove all uses of legacy `apply` in Proof Mode

!1077 · created Sep 23, 2024 by Robbert Krebbers
- 8
updated Oct 10, 2024
Use gmake for BSD systems

!1061 · created Jul 31, 2024 by Yiyun Liu
- 1
updated Jul 31, 2024
Add `and_own` lemma for handling `own γ x ∧ own γ y`

!1052 · created Jun 10, 2024 by tjhance
- 18
updated Dec 06, 2024
Prevent iFrame from instantiating existentials under updates.

!1041 · created Mar 12, 2024 by Janno
- 15
updated Aug 20, 2024
Do not use eta-expansion in `into_forall_forall`.

!1020 · created Nov 15, 2023 by Robbert Krebbers
- 13
updated Mar 05, 2024
More documentation about _1 and _2 lemmas.

!1008 · created Oct 18, 2023 by Robbert Krebbers
- 2
updated Oct 20, 2023
Add notations for `<affine> ⌜ ⌝` and friends.

!1007 · created Oct 15, 2023 by Robbert Krebbers
- 12
updated Oct 17, 2023
Add `IsOp` instances for `gset`, `coPset`, `gmultiset`

!1004 · created Oct 11, 2023 by Ike Mulder
- 5
updated Nov 10, 2023
Draft: Make sure that `?` in `iIntros`/`iDestruct` generate names that are not in the pattern

!992 · created Oct 03, 2023 by Robbert Krebbers
- 9
updated Oct 04, 2023
Avoid using specific `G` classes for locks, always use the projection `lockG` of `lock`.

!980 · created Aug 29, 2023 by Robbert Krebbers
- 7
updated Aug 30, 2023
Draft: experiment: use coq's ability to infer more canonical structures

!972 · created Aug 11, 2023 by Ralf Jung
S-blocked
- 3
updated Aug 28, 2023
Draft: Attempted fix for #539, solving slow type-checking of nested `●` terms

!971 · created Aug 10, 2023 by Ike Mulder
- 16
updated Aug 28, 2023
Draft: Avoid `Local Ltac` and `Local Tactic Notation` in proofmode.

!953 · created Jul 24, 2023 by Robbert Krebbers
- 7
updated Aug 05, 2023
Make bi fields non-canonical

!933 · created May 26, 2023 by Paolo G. Giarrusso
S-blocked
- 34
updated Oct 13, 2023
Draft: Improve validity information received from `iCombine`ing `own`s

!930 · created May 25, 2023 by Ike Mulder
- 22
updated Nov 10, 2023
add fixpoint lemmas for plain and absorbing

!903 · created Apr 01, 2023 by William Mansky
- 19
updated Apr 02, 2024