Merge branch 'master' of gitlab.mpi-sws.org:FP/stacked-borrows

theories/sim/cmra.v

@@ -298,3 +298,6 @@ Proof. intros Eq. rewrite lookup_core Eq /core /= core_id //. Qed.
 
 Definition res_callState (c: call_id) (cs: call_state) : resUR :=
   ((ε, {[c := to_callStateR cs]}), ε).
+
+Definition res_mapsto l s stk : resUR :=
+  (ε, {[ l := to_locStateR (lsLocal s stk)]}).

theories/sim/refl_step.v

@@ -7,9 +7,6 @@ Set Default Proof Using "Type".
 
 (** MEM STEP -----------------------------------------------------------------*)
 
-Definition res_alloc_local l s stk : resUR :=
-  (ε, {[ l := to_locStateR (lsLocal s stk)]}).
-
 Lemma sim_body_alloc_local fs ft r n T σs σt Φ :
   let l := (fresh_block σt.(shp), 0) in
   let t := (Tagged σt.(snp)) in
@@ -19,7 +16,7 @@ Lemma sim_body_alloc_local fs ft r n T σs σt Φ :
   let σt' := mkState (init_mem l (tsize T) σt.(shp))
                      (init_stacks σt.(sst) l (tsize T) t) σt.(scs)
                      (S σt.(snp)) σt.(snc) in
-  let r' : resUR := res_alloc_local l ScPoison (init_stack t) in
+  let r' : resUR := res_mapsto l ScPoison (init_stack t) in
   Φ (r ⋅ r') n (PlaceR l t T) σs' (PlaceR l t T) σt' : Prop →
   r ⊨{n,fs,ft} (Alloc T, σs) ≥ (Alloc T, σt) : Φ.
 Proof.