diff options
Diffstat (limited to 'scheduling')
| -rw-r--r-- | scheduling/RTLpathScheduler.v | 2 | ||||
| -rw-r--r-- | scheduling/RTLpathScheduleraux.ml | 1 |
2 files changed, 1 insertions, 2 deletions
diff --git a/scheduling/RTLpathScheduler.v b/scheduling/RTLpathScheduler.v index 1baf3fca..31680256 100644 --- a/scheduling/RTLpathScheduler.v +++ b/scheduling/RTLpathScheduler.v @@ -180,7 +180,7 @@ Proof. apply H in EQ2. rewrite EQ2. simpl. repeat (constructor; eauto). exploit function_equiv_checker_entrypoint. eapply EQ4. rewrite EQ2. intuition. -Qed. +Qed. Record match_function (dupmap: PTree.t node) (f1 f2: RTLpath.function): Prop := { preserv_fnsig: fn_sig f1 = fn_sig f2; diff --git a/scheduling/RTLpathScheduleraux.ml b/scheduling/RTLpathScheduleraux.ml index 5f0858f7..6dc00227 100644 --- a/scheduling/RTLpathScheduleraux.ml +++ b/scheduling/RTLpathScheduleraux.ml @@ -304,7 +304,6 @@ let rec do_schedule code pm = function (*debug "\nSchedule to apply: "; print_arrayp schedule;*) (*debug "\nNew Code: "; print_code new_code;*) debug "\n"; - (*debug_flag := false; *) do_schedule new_code pm lsb end |