Commit a9034293 authored by Robbert Krebbers's avatar Robbert Krebbers

The tactics setoid_subst x and cofe_subst now also clear x.

parent c9ae33d4
...@@ -134,9 +134,9 @@ Next Obligation. ...@@ -134,9 +134,9 @@ Next Obligation.
assert ( x2', y ={n2}= x1 x2' x2 x2') as (x2'&Hy&?). assert ( x2', y ={n2}= x1 x2' x2 x2') as (x2'&Hy&?).
{ destruct Hxy as [z Hy]; exists (x2 z); split; eauto using @ra_included_l. { destruct Hxy as [z Hy]; exists (x2 z); split; eauto using @ra_included_l.
apply dist_le with n1; auto. by rewrite (associative op) -Hx Hy. } apply dist_le with n1; auto. by rewrite (associative op) -Hx Hy. }
exists x1, x2'; split_ands; [done| |]. clear Hxy; cofe_subst y; exists x1, x2'; split_ands; [done| |].
* cofe_subst y; apply uPred_weaken with x1 n1; eauto using cmra_valid_op_l. * apply uPred_weaken with x1 n1; eauto using cmra_valid_op_l.
* cofe_subst y; apply uPred_weaken with x2 n1; eauto using cmra_valid_op_r. * apply uPred_weaken with x2 n1; eauto using cmra_valid_op_r.
Qed. Qed.
Program Definition uPred_wand {M} (P Q : uPred M) : uPred M := Program Definition uPred_wand {M} (P Q : uPred M) : uPred M :=
......
...@@ -218,7 +218,7 @@ Ltac setoid_subst_aux R x := ...@@ -218,7 +218,7 @@ Ltac setoid_subst_aux R x :=
try match H' with H => fail 2 end; try match H' with H => fail 2 end;
setoid_rewrite H in H' setoid_rewrite H in H'
end; end;
clear H clear x H
end. end.
Ltac setoid_subst := Ltac setoid_subst :=
repeat match goal with repeat match goal with
......
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