fix some lifting-related opens

kth-step · Mar 4, 2024 · 8d0a2b0 · 8d0a2b0
1 parent b373aa8
commit 8d0a2b0
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 2 deletions.
diff --git a/src/tools/lifter/bir_inst_liftingLib.sml b/src/tools/lifter/bir_inst_liftingLib.sml
@@ -8,6 +8,10 @@ functor bir_inst_liftingFunctor (MD : sig val mr : bir_lifting_machinesLib.bmr_r
 (* dependencies *)
 (* ================================================ *)
 open HolKernel boolLib liteLib simpLib Parse bossLib;
+
+(* FIXME: needed to avoid quse errors *)
+open m0_stepLib;
+
 open bir_inst_liftingTheory
 open bir_lifting_machinesTheory
 open bir_lifting_machinesLib bir_lifting_machinesLib_instances;

diff --git a/src/tools/lifter/bir_lifting_machinesLib_instances.sml b/src/tools/lifter/bir_lifting_machinesLib_instances.sml
@@ -3,14 +3,14 @@ structure bir_lifting_machinesLib_instances :>
 struct
 (* For compilation: *)
 open HolKernel boolLib liteLib simpLib Parse bossLib;
+(* Function libraries from examples/l3-machine-code: *)
+open m0_stepLib arm8_stepLib riscv_stepLib
 (* Local theories: *)
 open bir_exp_liftingLib bir_lifting_machinesTheory
      bir_nzcv_introsTheory bir_arm8_extrasTheory bir_m0_extrasTheory
      bir_riscv_extrasTheory
 (* Local function libraries: *)
 open bir_lifting_machinesLib;
-(* Function libraries from examples/l3-machine-code: *)
-open arm8_stepLib m0_stepLib riscv_stepLib
 
 (* Abbreviations used in this file:
  * BMR: BIR machine record. *)