Add diminish_srw_ss to build ARMv7 enc proofs

The other encorder proofs do not seem to be affected.
CakeML · Mar 30, 2020 · c258b1a · c258b1a
1 parent a7ed4e2
commit c258b1a
Showing 1 changed file with 2 additions and 0 deletions.
diff --git 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