Get some examples to build again

CakeML · Aug 6, 2020 · 0b23296 · 0b23296
1 parent bf4894f
commit 0b23296
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 0 deletions.
diff --git a/examples/array_searchProgScript.sml b/examples/array_searchProgScript.sml
@@ -7,6 +7,10 @@ open basisProgTheory quicksortProgTheory ArrayProofTheory UnsafeProgTheory Unsaf
 
 val _ = new_theory "array_searchProg";
 
+val _ = temp_delsimps ["NORMEQ_CONV"]
+val _ = diminish_srw_ss ["ABBREV"]
+val _ = set_trace "BasicProvers.var_eq_old" 1
+
 val _ = translation_extends "UnsafeProg";
 
 fun basis_st () = get_ml_prog_state ()

diff --git a/examples/diffScript.sml b/examples/diffScript.sml
@@ -6,6 +6,10 @@ open preamble lcsTheory mlintTheory mlstringTheory;
 
 val _ = new_theory "diff";
 
+val _ = temp_delsimps ["NORMEQ_CONV"]
+val _ = diminish_srw_ss ["ABBREV"]
+val _ = set_trace "BasicProvers.var_eq_old" 1
+
 fun drule0 th =
   first_assum(mp_tac o MATCH_MP (ONCE_REWRITE_RULE[GSYM AND_IMP_INTRO] th))
 

diff --git a/examples/quicksortProgScript.sml b/examples/quicksortProgScript.sml
@@ -7,6 +7,10 @@ open basisProgTheory ArrayProofTheory
 
 val _ = new_theory "quicksortProg";
 
+val _ = temp_delsimps ["NORMEQ_CONV"]
+val _ = diminish_srw_ss ["ABBREV"]
+val _ = set_trace "BasicProvers.var_eq_old" 1
+
 val _ = translation_extends"basisProg";
 
 (* TODO: move *)