fix Holmakefile

CakeML · Jun 14, 2022 · 711bd65 · 711bd65
1 parent 5591164
commit 711bd65
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 4 deletions.
diff --git a/examples/Holmakefile b/examples/Holmakefile
@@ -1,4 +1,5 @@
-INCLUDES = $(CAKEMLDIR)/developers $(CAKEMLDIR)/misc\
+INCLUDES = $(HOLDIR)/examples/formal-languages/regular $(HOLDIR)/examples/bootstrap \
+					 $(CAKEMLDIR)/developers $(CAKEMLDIR)/misc\
 					 $(CAKEMLDIR)/semantics $(CAKEMLDIR)/basis/pure $(CAKEMLDIR)/basis\
 					 $(CAKEMLDIR)/translator $(CAKEMLDIR)/characteristic
 

diff --git a/examples/pseudo_bool/array/pb_arrayProgScript.sml b/examples/pseudo_bool/array/pb_arrayProgScript.sml
@@ -123,8 +123,8 @@ Theorem check_cutting_arr_spec:
       ARRAY fmlv fmllsv *
         & (Fail_exn e ∧ check_cutting_list fmlls constr = NONE)))
 Proof
-  Induct_on`constr`>>
-  xcf"check_cutting_arr"(get_ml_prog_state ())
+  Induct_on`constr` >> rw[]>>
+  xcf "check_cutting_arr" (get_ml_prog_state ())
   >- ( (* Id *)
     fs[check_cutting_list_def,PB_CHECK_CONSTR_TYPE_def]>>
     xmatch>>
@@ -1048,7 +1048,7 @@ Proof
         xsimpl>>
         first_x_assum (irule_at Any)>>xsimpl>>
         first_x_assum (irule_at Any)>>xsimpl>>
-        simp[EqualityType_NUM_BOOL,all_goals_def])
+        simp[EqualityType_NUM_BOOL,all_goals_def])>>
       IF_CASES_TAC>>fs[]
       >- (
         xif>>asm_exists_tac>>xsimpl>>