Commit 42281a34 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Fix typo

parent aa81760b
Pipeline #2172 passed with stage
...@@ -17,7 +17,7 @@ Global Instance into_sep_mapsto l q v : ...@@ -17,7 +17,7 @@ Global Instance into_sep_mapsto l q v :
Proof. by rewrite /IntoSep heap_mapsto_op_split. Qed. Proof. by rewrite /IntoSep heap_mapsto_op_split. Qed.
Lemma tac_wp_alloc Δ Δ' N E j e v Φ : Lemma tac_wp_alloc Δ Δ' N E j e v Φ :
to_val e = Some v to_val e = Some v
(Δ heap_ctx N) nclose N E (Δ heap_ctx N) nclose N E
IntoLaterEnvs Δ Δ' IntoLaterEnvs Δ Δ'
( l, Δ'', ( l, Δ'',
...@@ -129,7 +129,7 @@ Tactic Notation "wp_load" := ...@@ -129,7 +129,7 @@ Tactic Notation "wp_load" :=
|solve_ndisj |solve_ndisj
|apply _ |apply _
|let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in |let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?" iAssumptionCore || fail "wp_load: cannot find" l "↦ ?"
|wp_finish] |wp_finish]
| _ => fail "wp_load: not a 'wp'" | _ => fail "wp_load: not a 'wp'"
end. end.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment