Fix rebinds

CakeML · Oct 17, 2023 · 626c628 · 626c628
1 parent 8bccfa7
commit 626c628
Show file tree

Hide file tree

Showing 5 changed files with 8 additions and 7 deletions.
diff --git a/compiler/bootstrap/translation/arm8ProgScript.sml b/compiler/bootstrap/translation/arm8ProgScript.sml
@@ -472,8 +472,8 @@ val res = translate def;
 val _ = translate (valid_immediate_def |> SIMP_RULE bool_ss
 [IN_INSERT,NOT_IN_EMPTY]|> econv)
 
-Theorem arm8_config_v_thm = translate (arm8_config_def |> SIMP_RULE bool_ss
-[IN_INSERT,NOT_IN_EMPTY]|> econv)
+Theorem arm8_config_v_thm[allow_rebind] =
+  translate (arm8_config_def |> SIMP_RULE bool_ss [IN_INSERT,NOT_IN_EMPTY]|> econv)
 
 val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 

diff --git a/compiler/bootstrap/translation/mipsProgScript.sml b/compiler/bootstrap/translation/mipsProgScript.sml
@@ -381,8 +381,8 @@ val res = CONJUNCTS d1 |> map SPEC_ALL |> map translate;
 
 val res = translate def;
 
-Theorem mips_config_v_thm = translate (mips_config_def |> SIMP_RULE bool_ss
-[IN_INSERT,NOT_IN_EMPTY]|> econv)
+Theorem mips_config_v_thm[allow_rebind] = translate
+  (mips_config_def |> SIMP_RULE bool_ss [IN_INSERT,NOT_IN_EMPTY]|> econv);
 
 val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 

diff --git a/compiler/bootstrap/translation/riscvProgScript.sml b/compiler/bootstrap/translation/riscvProgScript.sml
@@ -364,7 +364,8 @@ val res = CONJUNCTS d1 |> map SPEC_ALL |> map translate;
 
 val res = translate def;
 
-Theorem riscv_config_v_thm = translate (riscv_config_def |> SIMP_RULE bool_ss [IN_INSERT, NOT_IN_EMPTY]|> econv);
+Theorem riscv_config_v_thm[allow_rebind] = translate
+  (riscv_config_def |> SIMP_RULE bool_ss [IN_INSERT, NOT_IN_EMPTY]|> econv);
 
 val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 

diff --git a/compiler/bootstrap/translation/to_target32ProgScript.sml b/compiler/bootstrap/translation/to_target32ProgScript.sml
@@ -295,7 +295,7 @@ val monadic_enc32_enc_sec_hash_32_ls_side_def = Q.prove(`
   simp[Once (fetch "-" "monadic_enc32_enc_sec_hash_32_ls_side_def")]>>
   metis_tac[monadic_enc32_enc_line_hash_32_ls_side_def]);
 
-Theorem monadic_enc32_enc_secs_32_side_def = Q.prove(`
+Theorem monadic_enc32_enc_secs_32_side_def[allow_rebind] = Q.prove(`
   monadic_enc32_enc_secs_32_side a b c ⇔ T`,
   EVAL_TAC>>
   rw[]>>

diff --git a/compiler/bootstrap/translation/x64ProgScript.sml b/compiler/bootstrap/translation/x64ProgScript.sml
@@ -500,7 +500,7 @@ val res = CONJUNCTS d1 |> map SPEC_ALL |> map translate;
 
 val res = translate def;
 
-Theorem x64_config_v_thm = translate (x64_config_def |> gconv);
+Theorem x64_config_v_thm[allow_rebind] = translate (x64_config_def |> gconv);
 
 val () = Feedback.set_trace "TheoryPP.include_docs" 0;