Commit 6823251d authored by Ralf Jung's avatar Ralf Jung
Browse files

remove an outdated comment

parent 1e40d59b
......@@ -94,7 +94,6 @@ Lemma insert_idN n m i x :
m !! i {n} Some x <[i:=x]>m {n} m.
Proof. intros (y'&?&->)%dist_Some_inv_r'. by rewrite insert_id. Qed.
(** Internalized properties *)
End ofe.
Global Instance map_seq_ne {A : ofe} start :
......
Supports Markdown
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