Commit 42cb296d authored by Ralf Jung's avatar Ralf Jung

minor nits

parent f519685e
...@@ -263,7 +263,7 @@ Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 : ...@@ -263,7 +263,7 @@ Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
fill_item Ki1 e1 = fill_item Ki2 e2 Ki1 = Ki2. fill_item Ki1 e1 = fill_item Ki2 e2 Ki1 = Ki2.
Proof. Proof.
destruct Ki1, Ki2; intros; try discriminate; simplify_equality'; destruct Ki1, Ki2; intros; try discriminate; simplify_equality';
repeat match goal with try match goal with
| H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H | H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H
end; auto. end; auto.
Qed. Qed.
...@@ -278,7 +278,7 @@ Proof. ...@@ -278,7 +278,7 @@ Proof.
intros Hfill Hred Hnval; revert K' Hfill. intros Hfill Hred Hnval; revert K' Hfill.
induction K as [|Ki K IH]; simpl; intros K' Hfill; auto using prefix_of_nil. induction K as [|Ki K IH]; simpl; intros K' Hfill; auto using prefix_of_nil.
destruct K' as [|Ki' K']; simplify_equality'. destruct K' as [|Ki' K']; simplify_equality'.
{ destruct (proj1 (eq_None_not_Some (to_val (fill K e1)))); { exfalso; apply (eq_None_not_Some (to_val (fill K e1)));
eauto using fill_not_val, head_ctx_step_val. } eauto using fill_not_val, head_ctx_step_val. }
cut (Ki = Ki'); [naive_solver eauto using prefix_of_cons|]. cut (Ki = Ki'); [naive_solver eauto using prefix_of_cons|].
eauto using fill_item_no_val_inj, values_head_stuck, fill_not_val. eauto using fill_item_no_val_inj, values_head_stuck, fill_not_val.
......
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