From c258b1a13e66d1a4a064fbf7bee9ef20eb899d07 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Mon, 30 Mar 2020 15:39:28 +0200 Subject: [PATCH] Add diminish_srw_ss to build ARMv7 enc proofs The other encorder proofs do not seem to be affected. --- compiler/encoders/arm7/proofs/arm7_targetProofScript.sml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/compiler/encoders/arm7/proofs/arm7_targetProofScript.sml b/compiler/encoders/arm7/proofs/arm7_targetProofScript.sml index f1b31b46fb..ca20b1ccbd 100644 --- a/compiler/encoders/arm7/proofs/arm7_targetProofScript.sml +++ b/compiler/encoders/arm7/proofs/arm7_targetProofScript.sml @@ -982,6 +982,8 @@ val arm7_target_ok = Q.prove ( val print_tac = asmLib.print_tac "correct" +val _ = diminish_srw_ss ["NORMEQ_ss"] + Theorem arm7_encoder_correct: encoder_correct arm7_target Proof