diff options
Diffstat (limited to 'scheduling/RTLpathScheduler.v')
| -rw-r--r-- | scheduling/RTLpathScheduler.v | 2 |
1 files changed, 1 insertions, 1 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; |