sig
  val global_sdefs : SyntaxDef.syntax_def list Pervasives.ref
  val string_tp : Term.term
  val additional_xslt_name : string
  val list_nil_name : string
  val list_cons_name : string
  val list_nil_sd : SyntaxDef.syntax_def
  val list_cons_sd : SyntaxDef.syntax_def
  val hlist_empty_name : string
  val hlist_one_name : string
  val hlist_tp : Term.term
  val hlist_name : string
  val hlist_cons_name : string
  val bit_sd : SyntaxDef.syntax_def
  val bit_0_cons_name : string
  val bit_tp : Term.term
  val bit_name : string
  val bit_1_cons_name : string
  val char_cons_name : string
  val char_name : string
  val char_tp : Term.term
  val list_tp : Term.term -> Term.term
  val list_tp_name : string
  val list_sd : SyntaxDef.syntax_def
  val list_tp_a : Term.term
  val string_name : string
  val string_cons_name : string
  val boolean_true_name : string
  val boolean_name : string
  val boolean_tp : Term.term
  val boolean_sd : SyntaxDef.syntax_def
  val boolean_false_name : string
  val boolean_true_sd : SyntaxDef.syntax_def
  val boolean_false_sd : SyntaxDef.syntax_def
  val term_type_var_name : string
  val term_type_var_b_name : string
  val term_tp : Term.term
  val term_tp_name : string
  val term_var_cons_name : string
  val term_term_cons_name : string
  val rewrite_rule_cons_name : string
  val ground_rewrite_rule_cons_name : string
  val rewrite_rule_name : string
  val rewrite_rule_tp : Term.term
  val let_be_name : string
  val let_ground_be_name : string
  val input_rewrite_rule_tp : Term.term
  val input_rewrite_rule_name : string
  val let_major_be_name : string
  val let_major_ground_be_name : string
  val priority_input_rewrite_rule_tp : Term.term
  val priority_input_rewrite_rule_name : string
  val fun_definition_cons_name : string
  val fun_definition_name : string
  val fun_definition_tp : Term.term
  val syntax_element_str_name : string
  val syntax_element_name : string
  val syntax_element_tp : Term.term
  val syntax_element_tpcons_name : string
  val syntax_element_list_elem_name : string
  val syntax_element_list_tp : Term.term
  val syntax_element_list_name : string
  val syntax_element_list_cons_name : string
  val syntax_definition_tp : Term.term
  val syntax_definition_name : string
  val syntax_definition_decl_name : string
  val syntax_definition_var_name : string
  val syntax_definition_var_op_name : string
  val syntax_definition_type_var_name : string
  val syntax_definition_type_var_b_name : string
  val parsed_tvar_name : string
  val parsed_tvar_b_name : string
  val parsed_tvar_tp : Term.term
  val universal_tvar_name : string
  val universal_tvar_b_name : string
  val brackets_name : string
  val verbatim_name : string
  val if_then_else_name : string
  val glb_name : string
  val assign_name : string
  val string_quote_name : string
  val close_context_name : string
  val path_library_name : string
  val path_file_name : string
  val load_file_name : string
  val set_prop_name : string
  val code_as_term_name : string
  val get_nonvar_definitions_name : string
  val eq_bool_name : string
  val ternary_truth_value_tp : Term.term
  val ternary_unknown_name : string
  val exception_name : string
  val is_level_name : string -> bool
  val value_level_name : string
  val value_pref : Term.term -> Term.term
  val level_E_name : string
  val level_E_pref : Term.term -> Term.term
  val level_D_name : string
  val level_D_pref : Term.term -> Term.term
  val level_C_name : string
  val level_C_pref : Term.term -> Term.term
  val level_B_name : string
  val level_B_pref : Term.term -> Term.term
  val level_A_name : string
  val level_A_pref : Term.term -> Term.term
  val is_level_ind_name : string -> bool
  val value_i_name : string
  val level_E_i_name : string
  val level_D_i_name : string
  val level_C_i_name : string
  val level_B_i_name : string
  val level_A_i_name : string
  val integer_of_level : Term.term -> int
  val remove_sharing : Term.term -> Term.term
  val needs_brackets : required:Term.term -> provided:Term.term -> bool
end