Fix data_to_word_assignProof given integer$Num rewrites changes

CakeML · Jan 30, 2024 · b76383b · b76383b
1 parent 82aae5e
commit b76383b
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/compiler/backend/proofs/data_to_word_assignProofScript.sml b/compiler/backend/proofs/data_to_word_assignProofScript.sml
@@ -5980,7 +5980,7 @@ val BIT_Lemma2 = prove(
 
 Theorem assign_WordFromInt:
    op = WordFromInt ==> ^assign_thm_goal
-Proof
+Proof[exclude_simps = INT_OF_NUM NUM_EQ0]
   rpt strip_tac \\ drule0 (evaluate_GiveUp2 |> GEN_ALL) \\ rw [] \\ fs []
   \\ `t.termdep <> 0` by fs[]
   \\ asm_rewrite_tac [] \\ pop_assum kall_tac
@@ -11504,7 +11504,7 @@ QED
 
 Theorem assign_UpdateByte:
    op = UpdateByte ==> ^assign_thm_goal
-Proof
+Proof[exclude_simps = INT_OF_NUM NUM_EQ0]
   rpt strip_tac \\ drule0 (evaluate_GiveUp |> GEN_ALL) \\ rw [] \\ fs []
   \\ `t.termdep <> 0` by fs[]
   \\ rpt_drule0 state_rel_cut_IMP