Commit bb4b373d authored by Ralf Jung's avatar Ralf Jung
Browse files

fix use of auto-generated names

parent cfcf9918
...@@ -436,7 +436,8 @@ Section properties. ...@@ -436,7 +436,8 @@ Section properties.
(k, ε) ~l~> (k', m) (k, ε) ~l~> (k', m)
(l ++ k, ε) ~l~> (l ++ k', replicate (length l) ε ++ m). (l ++ k, ε) ~l~> (l ++ k', replicate (length l) ε ++ m).
Proof. Proof.
remember (app_l_local_update l k k' ε m) as HH. clear HeqHH. move: HH. remember (app_l_local_update l k k' ε m) as HH eqn:HeqHH.
clear HeqHH. move: HH.
by rewrite take_nil drop_nil ucmra_unit_left_id. by rewrite take_nil drop_nil ucmra_unit_left_id.
Qed. Qed.
...@@ -484,7 +485,7 @@ Section properties. ...@@ -484,7 +485,7 @@ Section properties.
move: HLen. clear. move: HLen. clear.
intros HLen. move: n. apply equiv_dist, list_equiv_lookup. intros HLen. move: n. apply equiv_dist, list_equiv_lookup.
intros i. rewrite list_lookup_op. intros i. rewrite list_lookup_op.
remember length as L. remember length as L eqn:HeqL.
destruct (decide (i < L m''))%nat as [E|E]. destruct (decide (i < L m''))%nat as [E|E].
- subst. apply lookup_lt_is_Some in E as [? HEl]. - subst. apply lookup_lt_is_Some in E as [? HEl].
rewrite HEl. rewrite HEl.
......
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