Commit 8957c470 authored by Robbert Krebbers's avatar Robbert Krebbers

Remove useless later.

parent 9a44a2d9
......@@ -220,7 +220,7 @@ Fixpoint proto_interp {Σ} (vs : list val) (p1 p2 : iProto Σ) : iProp Σ :=
| v :: vs => pc p2',
p2 proto_message Receive pc
pc v (proto_eq_next p2')
proto_interp vs p1 p2'
proto_interp vs p1 p2'
Arguments proto_interp {_} _ _%proto _%proto : simpl nomatch.
......@@ -593,7 +593,7 @@ Section proto.
{ iRewrite -"Heval". by rewrite /iProto_dual proto_map_message. }
rewrite /= proto_eq_next_dual; auto.
- iDestruct "Heval" as (pc' p2') "(Heq & Hc' & Heval)".
iExists pc', p2'. iFrame "Heq Hc'". iNext. iApply ("IH" with "Heval Hc").
iExists pc', p2'. iFrame "Heq Hc'". iApply ("IH" with "Heval Hc").
Lemma proto_interp_recv v vs p1 pc :
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