diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref index b17918505b6f994a2fb86d16a8f92fcbb5eb98c3..784aad7a5d476affff351ff603bfc716ca77637a 100644 --- a/tests/heap_lang.ref +++ b/tests/heap_lang.ref @@ -195,7 +195,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or Σ : gFunctors heapG0 : heapG Σ E1, E2 : coPset - P : iPropI Σ + P : iProp Σ ============================ Atomic (stuckness_to_atomicity NotStuck) (#() #()) diff --git a/tests/heap_lang.v b/tests/heap_lang.v index 5196629e5acfa56375056b04dd34c9ac7bbdec0c..2401114aaba70d51630b67c1c45eb2ff427b0205 100644 --- a/tests/heap_lang.v +++ b/tests/heap_lang.v @@ -325,6 +325,7 @@ End inv_mapsto_tests. Section atomic. Context `{!heapG Σ}. + Implicit Types P Q : iProp Σ. (* These tests check if a side-condition for [Atomic] is generated *) Check "wp_iMod_fupd_atomic".