Merge pull request #1240 from CakeML/use-no_sig_docs

Use no_sig_docs instead of `Feedback.set_trace "TheoryPP.include_docs" 0`

Author: tanyongkiam

basis/pure/basis_cvScript.sml

@@ -1,7 +1,7 @@
 (*
   Translation of basis types and functions for use with cv_compute.
 *)
-Theory basis_cv
+Theory basis_cv[no_sig_docs]
 Ancestors
   cv_std
 Libs
@@ -51,4 +51,3 @@ QED
 val _ = cv_trans (mlintTheory.toString_def |> SRULE [Num_ABS]);
 val _ = cv_trans mlintTheory.num_to_str_def;
 
-val _ = Feedback.set_trace "TheoryPP.include_docs" 0;

compiler/bootstrap/translation/ag32ProgScript.sml

@@ -1,7 +1,7 @@
 (*
   Translate the ag32 instruction encoder and ag32-specific config.
 *)
-Theory ag32Prog
+Theory ag32Prog[no_sig_docs]
 Ancestors
   evaluate ml_translator ag32_target ag32 arm7Prog[qualified]
 Libs
@@ -143,6 +143,5 @@ val res = translate def;
 
 val r = translate (format_def ag32_config_def);
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 
 val _ = (ml_translatorLib.clean_on_exit := true);

compiler/bootstrap/translation/arm7ProgScript.sml

@@ -1,7 +1,7 @@
 (*
   Translate the ARMv7 instruction encoder and ARMv7-specific config.
 *)
-Theory arm7Prog
+Theory arm7Prog[no_sig_docs]
 Ancestors
   evaluate ml_translator from_pancake32Prog arm7_target arm
   to_target32Prog[qualified]
@@ -485,7 +485,6 @@ val res = translate def;
 
 val res = translate (arm7_config_def |> SIMP_RULE std_ss[valid_immediate_def] |> gconv)
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 
 val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
 

compiler/bootstrap/translation/arm8ProgScript.sml

@@ -1,7 +1,7 @@
 (*
   Translate the ARMv8 instruction encoder and ARMv8-specific config.
 *)
-Theory arm8Prog
+Theory arm8Prog[no_sig_docs]
 Ancestors
   arm8_target arm8 evaluate ml_translator x64Prog
 Libs
@@ -515,7 +515,6 @@ val _ = translate (valid_immediate_def |> SIMP_RULE bool_ss
 Theorem arm8_config_v_thm[allow_rebind] =
   translate (arm8_config_def |> SIMP_RULE bool_ss [IN_INSERT,NOT_IN_EMPTY]|> econv)
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 
 val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
 

compiler/bootstrap/translation/basis_defProgScript.sml

@@ -1,7 +1,7 @@
 (*
   Translate the basis library term.
 *)
-Theory basis_defProg
+Theory basis_defProg[no_sig_docs]
 Ancestors
   ml_translator sexp_parserProg
 Libs
@@ -21,4 +21,3 @@ val res = translate basisProgTheory.basis_def;
 
 val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0;

compiler/bootstrap/translation/caml_lexProgScript.sml

@@ -1,7 +1,7 @@
 (*
   Translation of the OCaml lexer.
  *)
-Theory caml_lexProg
+Theory caml_lexProg[no_sig_docs]
 Ancestors
   caml_lex parserProg ml_translator
 Libs
@@ -170,6 +170,5 @@ val r = translate (caml_lexTheory.next_sym_def |> REWRITE_RULE [GSYM sub_check_d
 
 val r = translate caml_lexTheory.lexer_fun_def;
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 
 val () = ml_translatorLib.clean_on_exit := true;

compiler/bootstrap/translation/caml_parserProgScript.sml

@@ -1,7 +1,7 @@
 (*
   Translation of the functions in caml_parserScript.sml
  *)
-Theory caml_parserProg
+Theory caml_parserProg[no_sig_docs]
 Ancestors
   misc[qualified] camlPEG camlPtreeConversion caml_parser
   ml_translator caml_lexProg
@@ -300,6 +300,5 @@ QED
 
 val _ = update_precondition run_side;
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 val () = ml_translatorLib.clean_on_exit := true;
 

compiler/bootstrap/translation/compiler32ProgScript.sml

@@ -1,7 +1,7 @@
 (*
   Finish translation of the 32-bit version of the compiler.
 *)
-Theory compiler32Prog
+Theory compiler32Prog[no_sig_docs]
 Ancestors
   compiler export ml_translator ag32Prog[qualified]
   arm7Prog[qualified] basis_ffi[qualified]
@@ -531,5 +531,4 @@ Theorem semantics_compiler32_prog =
   |> DISCH_ALL
   |> SIMP_RULE (srw_ss()) [AND_IMP_INTRO,GSYM CONJ_ASSOC]
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 val _ = ml_translatorLib.reset_translation(); (* because this translation won't be continued *)

compiler/bootstrap/translation/compiler64ProgScript.sml

@@ -1,7 +1,7 @@
 (*
   Finish translation of the 64-bit version of the compiler.
 *)
-Theory compiler64Prog
+Theory compiler64Prog[no_sig_docs]
 Ancestors
   mipsProg compiler export ml_translator basis_ffi[qualified]
 Libs
@@ -785,5 +785,4 @@ Theorem Decls_FRONT_compiler64_prog = th1
 
 Theorem LAST_compiler64_prog = EVAL “LAST compiler64_prog”;
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 val _ = ml_translatorLib.reset_translation(); (* because this translation won't be continued *)

compiler/bootstrap/translation/decodeProgScript.sml

@@ -1,7 +1,7 @@
 (*
   Translate the compiler's state decoder.
 *)
-Theory decodeProg
+Theory decodeProg[no_sig_docs]
 Ancestors
   num_list_enc_dec num_tree_enc_dec backend_enc_dec explorerProg
   ml_translator
@@ -260,7 +260,6 @@ val res = translate backend_inc_config_dec_def;
 
 val res = translate decode_backend_config_def;
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 
 val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);