Merge requests · Iris / RefinedC

Some more simplification instances

!38 · created Feb 17, 2021 by Michael Sammler
- MERGED
- 0
updated Feb 17, 2021
split out heap_loc_eq

!105 · created Aug 03, 2021 by Michael Sammler
- MERGED
- 0
updated Aug 03, 2021
Strengthen the [LocInBounds] infrastructure.

!22 · created Feb 01, 2021 by Rodolphe Lepigre
- MERGED
- Approved
- 11
updated Feb 02, 2021
Sugar in the front end + Coq pretty printing

!16 · created Jan 13, 2021 by Rodolphe Lepigre
- MERGED
- Approved
- 17
updated Jan 15, 2021
sync Makefile and CI with Iris

!1 · created Jul 16, 2020 by Ralf Jung
- MERGED
- 0
updated Jul 16, 2020
Tactic based on lia and autorewrite to solve location equality

!46 · created Feb 22, 2021 by Rodolphe Lepigre
- MERGED
- 15
updated Feb 24, 2021
Time/mem cast

!83 · created Jun 25, 2021 by Michael Sammler
- MERGED
- 0
updated Jul 15, 2021
try new version of unification

!30 · created Feb 12, 2021 by Michael Sammler
- MERGED
- 0
updated Feb 12, 2021
try removing pinning of conf-mpfr

!93 · created Jul 14, 2021 by Michael Sammler
- MERGED
- 0
updated Jul 14, 2021
Unfold instantiated evars on each liRStep.

!15 · created Jan 12, 2021 by Rodolphe Lepigre
- MERGED
- 1
updated Jan 12, 2021
Unfold more definitions in the side condition solver.

!23 · created Feb 02, 2021 by Rodolphe Lepigre
- MERGED
- Approved
- 0
updated Feb 03, 2021
Update Cerberus version.

!66 · created Jun 02, 2021 by Rodolphe Lepigre
- MERGED
- 0
updated Jun 02, 2021
update Iris

!136 · created May 13, 2022 by Michael Sammler
- MERGED
- 0
updated May 13, 2022
update iris

!68 · created Jun 14, 2021 by Michael Sammler
- MERGED
- 0
updated Jun 14, 2021
update to coq 8.13.2

!101 · created Jul 27, 2021 by Michael Sammler
- MERGED
- 0
updated Jul 27, 2021
Updated early alloc example

!84 · created Jul 05, 2021 by Michael Sammler
- MERGED
- 0
updated Jul 05, 2021
Upgrade README demo: it_max -> max_int.

!9 · created Dec 04, 2020 by Fengmin Zhu
- MERGED
- 1
updated Dec 04, 2020
upgrade to coq 8.14.0

!119 · created Oct 19, 2021 by Michael Sammler
- MERGED
- 2
updated Oct 19, 2021
Use multisuccess of typeclasses eauto to get rid of n parameter in FindInContext

!107 · created Aug 05, 2021 by Michael Sammler
- MERGED
- 0
updated Aug 05, 2021
Use separate inductives for allocation (refactoring).

!6 · created Dec 02, 2020 by Rodolphe Lepigre
- MERGED
- 11
updated Dec 02, 2020