diff options
Diffstat (limited to 'scheduling')
| -rw-r--r-- | scheduling/RTLpathSE_impl.v | 2 | ||||
| -rw-r--r-- | scheduling/RTLpathScheduleraux.ml | 8 |
2 files changed, 5 insertions, 5 deletions
diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v index 12aba56b..e21d7cd1 100644 --- a/scheduling/RTLpathSE_impl.v +++ b/scheduling/RTLpathSE_impl.v @@ -819,7 +819,7 @@ Proof. rewrite <- X, sok_local_set_sreg. intuition eauto. - destruct REF; intuition eauto. - generalize REF; intros (OKEQ & _). rewrite OKEQ in * |-; erewrite red_PTree_set_refines; eauto. - Qed. +Qed. Global Opaque hslocal_set_sreg. Local Hint Resolve hslocal_set_sreg_correct: wlp. diff --git a/scheduling/RTLpathScheduleraux.ml b/scheduling/RTLpathScheduleraux.ml index c2183937..6dc00227 100644 --- a/scheduling/RTLpathScheduleraux.ml +++ b/scheduling/RTLpathScheduleraux.ml @@ -298,11 +298,11 @@ let rec do_schedule code pm = function let new_code = apply_schedule code' sb schedule in begin (*debug_flag := true;*) + if code != code_exp then ( debug "Old Code: "; print_code code; - debug "Exp Code: "; print_code code_exp; - (*debug_flag := false; *) - debug "\nSchedule to apply: "; print_arrayp schedule; - debug "\nNew Code: "; print_code new_code; + debug "Exp Code: "; print_code code_exp); + (*debug "\nSchedule to apply: "; print_arrayp schedule;*) + (*debug "\nNew Code: "; print_code new_code;*) debug "\n"; do_schedule new_code pm lsb end |