aarch64 compiles again (but ccomp generates incorrect assembly)

1 files changed, 5 insertions, 5 deletions

diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v
index 5dec10e9..af069929 100644
--- a/aarch64/Asmgen.v
+++ b/aarch64/Asmgen.v
@@ -28,19 +28,19 @@ Local Open Scope error_monad_scope.
 Module Asmblock_TRANSF.
 (* STUB *)
 
-Definition ireg_of_preg (p : Asmblock.preg) : res ireg :=
+Definition ireg_of_preg (p : Asm.preg) : res ireg :=
   match p with
   | DR (IR' (RR1 r)) => OK r
   | _ => Error (msg "Asmgen.ireg_of_preg")
   end.
 
-Definition freg_of_preg (p : Asmblock.preg) : res freg :=
+Definition freg_of_preg (p : Asm.preg) : res freg :=
   match p with
   | DR (FR' r) => OK r
   | _ => Error (msg "Asmgen.freg_of_preg")
   end.
 
-Definition iregsp_of_preg (p : Asmblock.preg) : res iregsp :=
+Definition iregsp_of_preg (p : Asm.preg) : res iregsp :=
   match p with
   | DR (IR' r) => OK r
   | _ => Error (msg "Asmgen.iregsp_of_preg")
@@ -61,7 +61,7 @@ Definition basic_to_instruction (b: basic) : res Asm.instruction :=
                                             OK (Asm.Pfmovimmd rd' f)
 
   | PArith (PArithPP (Pmovk sz n pos) rd rs) =>
-    if (Asmblock.preg_eq rd rs) then (
+    if (Asm.preg_eq rd rs) then (
       do rd' <- ireg_of_preg rd;
       OK (Asm.Pmovk sz rd' n pos)
     ) else
@@ -359,4 +359,4 @@ Definition transf_program (p: Mach.program) : res Asm.program :=
   let mbp := Machblockgen.transf_program p in
   do mbp' <- PseudoAsmblockproof.transf_program mbp;
   do abp <- Asmblockgen.transf_program mbp';
-  Asmblock_TRANSF.transf_program abp.
+  Asmblock_TRANSF.transf_program abp.
\ No newline at end of file