From 95d972434bd4d3b6ee0d0f68c688920dafe14afc Mon Sep 17 00:00:00 2001 From: Justus Fasse Date: Wed, 18 Aug 2021 18:05:14 +0200 Subject: Match naming convention of surrounding code. --- scheduling/RTLpathSE_impl.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v index 71b446cc..40a05739 100644 --- a/scheduling/RTLpathSE_impl.v +++ b/scheduling/RTLpathSE_impl.v @@ -1845,10 +1845,10 @@ Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpa let (pc2, pc1) := m in (* creating the hash-consing tables *) DO hC_sval <~ hCons hSVAL;; - DO hc_scond <~ hCons hSCOND;; + DO hC_scond <~ hCons hSCOND;; DO hC_list_hsval <~ hCons hLSVAL;; DO hC_hsmem <~ hCons hSMEM;; - let hsexec := hsexec hC_sval.(hC) hC_list_hsval.(hC) hC_hsmem.(hC) hc_scond.(hC) in + let hsexec := hsexec hC_sval.(hC) hC_list_hsval.(hC) hC_hsmem.(hC) hC_scond.(hC) in (* performing the hash-consed executions *) XDEBUG pc1 (fun pc => DO name_pc <~ string_of_Z (Zpos pc);; RET ("entry-point of input superblock: " +; name_pc)%string);; DO hst1 <~ hsexec f pc1;; -- cgit