Merge remote-tracking branch 'origin/master' into x86-float

CakeML · Dec 30, 2017 · c5e294e · c5e294e
2 parents 9cbae90 + 4db3cb0
commit c5e294e
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/compiler/bootstrap/translation/x64ProgScript.sml b/compiler/bootstrap/translation/x64ProgScript.sml
@@ -93,7 +93,7 @@ val if_neq = Q.prove(`
 
 val fconv = SIMP_RULE (srw_ss()) [SHIFT_ZERO,case_ifs,case_ifs2,if_neq]
 
-val defaults = [x64_ast_def,x64_encode_def,encode_def,e_rm_reg_def,e_gen_rm_reg_def,e_ModRM_def,e_opsize_def,e_imm32_def,rex_prefix_def,x64_dec_fail_def,e_opc_def,e_rax_imm_def,e_rm_imm_def,asmSemTheory.is_test_def,x64_cmp_def,e_opsize_imm_def,e_imm8_def,e_rm_imm8_def,not_byte_def,e_imm16_def,e_imm64_def,Zsize_width_def,x64_bop_def,zreg2num_totalnum2zerg,e_imm_8_32_def,Zbinop_name2num_x64_sh,x64_sh_notZtest,exh_if_collapse,is_rax_zr_thm]
+val defaults = [x64_ast_def,x64_encode_def,encode_def,e_gen_rm_reg_def,e_ModRM_def,e_opsize_def,e_imm32_def,rex_prefix_def,x64_dec_fail_def,e_opc_def,e_rax_imm_def,e_rm_imm_def,asmSemTheory.is_test_def,x64_cmp_def,e_opsize_imm_def,e_imm8_def,e_rm_imm8_def,not_byte_def,e_imm16_def,e_imm64_def,Zsize_width_def,x64_bop_def,zreg2num_totalnum2zerg,e_imm_8_32_def,Zbinop_name2num_x64_sh,x64_sh_notZtest,exh_if_collapse,is_rax_zr_thm]
 
 val x64_enc_thms =
   x64_enc_def

diff --git a/compiler/encoders/x64/x64_targetLib.sml b/compiler/encoders/x64/x64_targetLib.sml
@@ -33,7 +33,7 @@ in
      (ERR "x64_encode_conv" "")
      (computeLib.compset_conv (wordsLib.words_compset())
       [computeLib.Defs
-         [x64_bop_def, x64_cmp_def, x64_sh_def, e_rm_reg_def, e_gen_rm_reg_def,
+         [x64_bop_def, x64_cmp_def, x64_sh_def, e_gen_rm_reg_def,
           e_ModRM_def, e_opsize_def, rex_prefix_def, e_opc_def, e_rm_imm8_def,
           e_opsize_imm_def, not_byte_def, e_rax_imm_def, e_rm_imm_def,
           e_imm_8_32_def, e_imm_def, e_imm8_def, e_imm16_def, e_imm32_def,