intro RTLpathWFcheck

1 files changed, 4 insertions, 4 deletions

diff --git a/scheduling/RTLpathScheduler.v b/scheduling/RTLpathScheduler.v
index beab405f..6f90b455 100644
--- a/scheduling/RTLpathScheduler.v
+++ b/scheduling/RTLpathScheduler.v
@@ -7,7 +7,7 @@ This module is inspired from [Duplicate] and [Duplicateproof]
 Require Import AST Linking Values Maps Globalenvs Smallstep Registers.
 Require Import Coqlib Maps Events Errors Op.
 Require Import RTL RTLpath RTLpathLivegen RTLpathLivegenproof RTLpathSE_theory RTLpathSE_impl.
-
+Require RTLpathWFcheck.
 
 Notation "'ASSERT' A 'WITH' MSG 'IN' B" := (if A then B else Error (msg MSG))
          (at level 200, A at level 100, B at level 200)
@@ -32,14 +32,14 @@ Extract Constant untrusted_scheduler => "RTLpathScheduleraux.scheduler".
 
 Program Definition function_builder (tfr: RTL.function) (tpm: path_map) : 
   { r : res RTLpath.function | forall f', r = OK f' -> fn_RTL f' = tfr} :=
-  match RTLpathLivegen.function_checker tfr tpm with
+  match RTLpathWFcheck.function_checker tfr tpm with
   | false => Error (msg "In function_builder: (tfr, tpm) is not wellformed")
   | true => OK {| fn_RTL := tfr; fn_path := tpm |}
   end.
 Next Obligation.
-  apply function_checker_path_entry. auto.
+  apply RTLpathWFcheck.function_checker_path_entry. auto.
 Defined. Next Obligation.
-  apply function_checker_wellformed_path_map. auto.
+  apply RTLpathWFcheck.function_checker_wellformed_path_map. auto.
 Defined.
 
 Definition entrypoint_check (dm: PTree.t node) (fr tfr: RTL.function) : res unit :=