Merge remote-tracking branch 'origin/master' into remove-cheats

Author: xrchz

basis/pure/mlvectorSyntax.sml

@@ -6,6 +6,8 @@ struct
 
 open HolKernel boolLib mlvectorTheory;
 
+val ERR = mk_HOL_ERR "mlvectorSyntax";
+
 fun mk_vector_type ty = Type.mk_thy_type{Thy="regexp_compiler",Tyop="vector",Args=[ty]};
 
 fun dest_vector_type ty =

characteristic/cfNormaliseLib.sml

@@ -3,6 +3,8 @@ structure cfNormaliseLib :> cfNormaliseLib = struct
 open preamble
 open astSyntax
 
+val ERR = mk_HOL_ERR "cfNormaliseLib";
+
 (* Normalisation pass.
 
    [normalise_prog] (and friends) implement a preprocessing pass on the

characteristic/cfTacticsBaseLib.sml

@@ -5,6 +5,8 @@ open preamble
 open set_sepTheory helperLib ConseqConv
 open quantHeuristicsTools
 
+val ERR = mk_HOL_ERR "cfTacticsBaseLib";
+
 structure Parse =
 struct
   open Parse

characteristic/cfTacticsLib.sml

@@ -7,6 +7,8 @@ open set_sepTheory cfAppTheory cfHeapsTheory cfTheory cfTacticsTheory
 open helperLib cfHeapsBaseLib cfHeapsLib cfTacticsBaseLib evarsConseqConvLib
 open cfAppLib cfSyntax semanticPrimitivesSyntax
 
+val ERR = mk_HOL_ERR "cfTacticsLib";
+
 fun constant_printer s _ _ _ (ppfns:term_pp_types.ppstream_funs) _ _ _ =
   let
     open Portable term_pp_types smpp

characteristic/evarsConseqConvLib.sml

@@ -4,6 +4,8 @@ struct
 open preamble
 open ConseqConv ConseqConvTheory quantHeuristicsTools
 
+val ERR = mk_HOL_ERR "evarsConseqConvLib";
+
 type evars = term list
 type term_with_evars = {term: term, evars: evars}
 type evars_instantiation = {instantiation: (term, term) subst,

compiler/backend/semantics/patSemScript.sml

@@ -453,7 +453,7 @@ val check =
   do_app_cases |> concl |> find_terms TypeBase.is_case
   |> List.map (#1 o strip_comb)
   |> List.all (fn tm => List.exists (same_const tm) [optionSyntax.option_case_tm, eq_result_CASE_tm])
-val () = if check then () else raise(ERR"patSem""do_app_cases failed")
+val () = if check then () else raise(mk_HOL_ERR"patSemTheory""do_app_cases""check failed")
 
 val do_app_cases_none = save_thm("do_app_cases_none",
   ``patSem$do_app s op vs = NONE`` |>

translator/ml_translatorLib.sml

@@ -15,6 +15,8 @@ open integerTheory intLib ml_optimiseTheory ml_pmatchTheory;
 open mlstringLib mlstringSyntax mlvectorSyntax packLib ml_progTheory ml_progLib
 local open integer_wordSyntax in end
 
+val ERR = mk_HOL_ERR "ml_translatorLib";
+
 val RW = REWRITE_RULE;
 val RW1 = ONCE_REWRITE_RULE;