Get a proof to build with an exclude_simps

CakeML · Nov 29, 2023 · a3cf8bb · a3cf8bb
1 parent 4ac0c7c
commit a3cf8bb
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/compiler/repl/evaluate_skipScript.sml b/compiler/repl/evaluate_skipScript.sml
@@ -341,7 +341,7 @@ Theorem pmatch_update:
           match_res_rel (λenv env'.
             LIST_REL (λ(n,v) (m,w). n = m ∧ v_rel fr ft fe v w)
                      env env') res res')
-Proof
+Proof[exclude_simps = option.OPTREL_NONE]
   ho_match_mp_tac pmatch_ind \\ rw [] \\ gvs [pmatch_def, v_rel_def, SF SFY_ss]
   >- (rw [] \\ gs [])
   >- (