Merge requests · Iris / Iris

Make* class tweaks

!842 · created Aug 13, 2022 by Ralf Jung
S-blocked
- Closed
- 40
updated Jul 25, 2023
Draft: Add simplification machinery for ✓ and ≼.

!771 · created Jan 10, 2022 by Ike Mulder
S-blocked
- Closed
- 18
updated May 25, 2023
Draft: Fix #497: avoid Hint Immediate

!869 · created Nov 24, 2022 by Paolo G. Giarrusso
S-blocked
- Closed
- 1
updated May 02, 2023
Dune build files

!820 · created Jul 23, 2022 by Paolo G. Giarrusso
S-blocked S-draft
- Closed
- 2
updated Mar 07, 2023
make Z.of_nat not a Coercion any more

!677 · created May 19, 2021 by Ralf Jung
S-blocked
- Closed
- 20
updated Jan 12, 2023
Prefix iDestruct automatic names with an underscore

!599 · created Dec 05, 2020 by Tej Chajed
S-blocked T-records
- Closed
- 20
updated Mar 18, 2021
WIP: Prepend introduction pattern `H.ipat`. 0 of 1 checklist item completed

!480 · created Jul 19, 2020 by Robbert Krebbers
S-blocked T-records
- Closed
- 23
updated Mar 18, 2021