diff options
Diffstat (limited to 'scheduling/RTLpathLivegen.v')
| -rw-r--r-- | scheduling/RTLpathLivegen.v | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/scheduling/RTLpathLivegen.v b/scheduling/RTLpathLivegen.v index 00ec3334..9f646ad0 100644 --- a/scheduling/RTLpathLivegen.v +++ b/scheduling/RTLpathLivegen.v @@ -61,8 +61,7 @@ Definition iinst_checker (pm: path_map) (alive: Regset.t) (i: instruction): opti Some (alive, pc') | Icond cond args ifso ifnot _ => ASSERT list_mem args alive IN - if Pos.eq_dec ifso ifnot then Some (alive, ifnot) - else exit_checker pm alive ifso (alive, ifnot) + exit_checker pm alive ifso (alive, ifnot) | _ => None end. @@ -73,7 +72,7 @@ Lemma iinst_checker_path_entry (pm: path_map) (alive: Regset.t) (i: instruction) iinst_checker pm alive i = Some res -> early_exit i = Some pc -> path_entry pm pc. Proof. - destruct i; simpl; try destruct Pos.eq_dec; try_simplify_someHyps; subst. + destruct i; simpl; try_simplify_someHyps; subst. inversion_ASSERT; try_simplify_someHyps. Qed. @@ -83,7 +82,7 @@ Lemma iinst_checker_default_succ (pm: path_map) (alive: Regset.t) (i: instructio default_succ i = Some pc. Proof. destruct i; simpl; try_simplify_someHyps; subst; - repeat (inversion_ASSERT); try destruct Pos.eq_dec; try_simplify_someHyps. + repeat (inversion_ASSERT); try_simplify_someHyps. intros; exploit exit_checker_res; eauto. intros; subst. simpl; auto. Qed. @@ -217,8 +216,7 @@ Proof. destruct (iinst_checker pm alive i) as [[alive0 pc0]|] eqn: CHECK1; simpl. - simpl; intros CHECK2 PC. eapply wf_last_node; eauto. destruct i; simpl in * |- *; intuition (subst; eauto); - try (generalize CHECK2 CHECK1; clear CHECK1 CHECK2; try (inversion_SOME path); - repeat inversion_ASSERT; try destruct Pos.eq_dec; try_simplify_someHyps). + try (generalize CHECK2 CHECK1; clear CHECK1 CHECK2; try (inversion_SOME path); repeat inversion_ASSERT; try_simplify_someHyps). intros PC CHECK1 CHECK2. intros; exploit exit_checker_res; eauto. intros X; inversion X. intros; subst; eauto. |