Commit a0399a74 authored by Robbert Krebbers's avatar Robbert Krebbers

Some missing simpls.

parent 64a3d258
......@@ -281,7 +281,7 @@ Tactic Notation "rel_alloc_l" "as" ident(l) constr(H) :=
[tac_bind_helper (* e = fill K' .. *)
|apply _ (* IntoLaterNEnvs _ _ _ *)
|solve_to_val (* to_val e' = Some v *)
|iIntros (l) H (* new goal *)].
|simpl; iIntros (l) H (* new goal *)].
Lemma tac_rel_alloc_r `{logrelG Σ} E1 E2 Δ Γ t' v' K' e t τ :
nclose specN E1
......@@ -335,7 +335,7 @@ Tactic Notation "rel_load_l" :=
|apply _ (* IntoLaterNenvs _ Δ1 Δ2 *)
|iAssumptionCore || fail 3 "rel_load_l: cannot find ? ↦ᵢ ?"
|simpl; reflexivity (* eres = fill K (of_val v) *)
| (* new goal *)].
|simpl (* new goal *)].
Lemma tac_rel_load_r `{logrelG Σ} 1 2 E1 E2 Δ Γ K i1 (l : loc) e t tres τ v :
nclose specN E1
......@@ -398,7 +398,7 @@ Tactic Notation "rel_store_l" :=
|iAssumptionCore || fail "rel_store_l: cannot find '? ↦ᵢ ?'"
|env_cbv; reflexivity || fail "rel_store_l: this should not happen"
|simpl; reflexivity (* eres = fill K () *)
|(* new goal *)].
|simpl (* new goal *)].
Lemma tac_rel_store_r `{logrelG Σ} 1 2 E1 E2 Δ Γ K i1 (l : loc) t' v' e t tres τ v :
nclose specN E1
......@@ -428,7 +428,7 @@ Tactic Notation "rel_store_r" :=
|iAssumptionCore || fail "rel_store_l: cannot find ? ↦ₛ ?"
|env_cbv; reflexivity || fail "rel_store_r: this should not happen"
|simpl; reflexivity (* tres = fill K () *)
|(* new goal *)].
|simpl (* new goal *)].
(* CAS *)
Tactic Notation "rel_cas_l_atomic" := rel_apply_l bin_log_related_cas_l.
......@@ -466,7 +466,7 @@ Tactic Notation "rel_cas_fail_r" :=
|try fast_done (* v v1 *)
|env_cbv; reflexivity || fail "rel_load_r: this should not happen"
|simpl; reflexivity (* tres = fill K false *)
|(* new goal *)].
|simpl (* new goal *)].
Lemma tac_rel_cas_suc_r `{logrelG Σ} 1 2 E1 E2 Δ Γ K i1 (l : loc) e t e1 e2 v1 v2 tres τ v :
......@@ -502,7 +502,7 @@ Tactic Notation "rel_cas_suc_r" :=
|try fast_done (* v = v1 *)
|env_cbv; reflexivity || fail "rel_load_r: this should not happen"
|simpl; reflexivity (* tres = fill K true *)
|(* new goal *)].
|simpl (* new goal *)].
(* TODO: move this to the tests folder *)
Section test.
......
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