diff options
Diffstat (limited to 'scheduling/RTLpathWFcheck.v')
| -rw-r--r-- | scheduling/RTLpathWFcheck.v | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/scheduling/RTLpathWFcheck.v b/scheduling/RTLpathWFcheck.v index eb7bdac7..63b914ec 100644 --- a/scheduling/RTLpathWFcheck.v +++ b/scheduling/RTLpathWFcheck.v @@ -36,8 +36,7 @@ Definition iinst_checker (pm: path_map) (i: instruction): option (node) := | Inop pc' | Iop _ _ _ pc' | Iload _ _ _ _ _ pc' | Istore _ _ _ _ pc' => Some (pc') | Icond cond args ifso ifnot _ => - if Pos.eq_dec ifso ifnot then Some (ifnot) - else exit_checker pm ifso ifnot + exit_checker pm ifso ifnot | _ => None end. @@ -47,7 +46,7 @@ Lemma iinst_checker_path_entry (pm: path_map) (i: instruction) res pc: iinst_checker pm 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. Qed. Lemma iinst_checker_default_succ (pm: path_map) (i: instruction) res pc: @@ -55,7 +54,7 @@ Lemma iinst_checker_default_succ (pm: path_map) (i: instruction) res pc: pc = res -> default_succ i = Some pc. Proof. - destruct i; simpl; try destruct Pos.eq_dec; try_simplify_someHyps; subst; + destruct i; simpl; try_simplify_someHyps; subst; repeat (inversion_ASSERT); try_simplify_someHyps. intros; exploit exit_checker_res; eauto. intros; subst. simpl; auto. @@ -123,8 +122,7 @@ Proof. intros CHECK PC. eapply wf_last_node; eauto. clear c pc PC. intros pc PC. destruct i; simpl in * |- *; intuition (subst; eauto); - try (generalize CHECK; clear CHECK; try (inversion_SOME path); - repeat inversion_ASSERT; try destruct Pos.eq_dec; try_simplify_someHyps). + try (generalize CHECK; clear CHECK; try (inversion_SOME path); repeat inversion_ASSERT; try_simplify_someHyps). intros X; exploit exit_checker_res; eauto. clear X. intros; subst; eauto. Qed. |